Nuprl Lemma : iff_transitivity

[P,Q,R:ℙ].  ((P ⇐⇒ Q)  (Q ⇐⇒ R)  (P ⇐⇒ R))


Proof




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

Latex:
\mforall{}[P,Q,R:\mBbbP{}].    ((P  \mLeftarrow{}{}\mRightarrow{}  Q)  {}\mRightarrow{}  (Q  \mLeftarrow{}{}\mRightarrow{}  R)  {}\mRightarrow{}  (P  \mLeftarrow{}{}\mRightarrow{}  R))



Date html generated: 2019_06_20-AM-11_16_41
Last ObjectModification: 2018_09_26-AM-10_24_20

Theory : core_2


Home Index