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