Nuprl Lemma : guard_functionality_wrt_iff
∀p,q:ℙ. ({p
⇐⇒ q}
⇒ {{p}
⇐⇒ {q}})
Proof
Definitions occuring in Statement :
prop: ℙ
,
guard: {T}
,
all: ∀x:A. B[x]
,
iff: P
⇐⇒ Q
,
implies: P
⇒ Q
Lemmas :
iff_wf
Latex:
\mforall{}p,q:\mBbbP{}. (\{p \mLeftarrow{}{}\mRightarrow{} q\} {}\mRightarrow{} \{\{p\} \mLeftarrow{}{}\mRightarrow{} \{q\}\})
Date html generated:
2015_07_22-PM-00_27_08
Last ObjectModification:
2015_01_28-AM-10_07_31
Home
Index