Nuprl Lemma : iff_symmetry

[A,B:ℙ].  (A ⇐⇒ ⇐⇒ ⇐⇒ A)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: iff: ⇐⇒ Q
Definitions unfolded in proof :  uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T prop: rev_implies:  Q
Lemmas referenced :  iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  independent_pairFormation lambdaFormation sqequalHypSubstitution productElimination thin hypothesisEquality independent_functionElimination hypothesis cut introduction extract_by_obid isectElimination Error :inhabitedIsType,  Error :universeIsType,  universeEquality

Latex:
\mforall{}[A,B:\mBbbP{}].    (A  \mLeftarrow{}{}\mRightarrow{}  B  \mLeftarrow{}{}\mRightarrow{}  B  \mLeftarrow{}{}\mRightarrow{}  A)



Date html generated: 2019_06_20-AM-11_15_52
Last ObjectModification: 2018_09_26-AM-10_23_50

Theory : core_2


Home Index