Nuprl Lemma : uiff_transitivity2

[P,Q,R:ℙ].  (uiff(P;Q)  (Q R ∈ ℙ uiff(P;R))


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) uall: [x:A]. B[x] prop: implies:  Q equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q prop: member: t ∈ T uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q uiff: uiff(P;Q)
Lemmas referenced :  iff_weakening_equal equal_wf uiff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut sqequalHypSubstitution hypothesis introduction extract_by_obid isectElimination thin equalityTransitivity equalitySymmetry independent_isectElimination productElimination independent_pairFormation independent_functionElimination hypothesisEquality hyp_replacement Error :applyLambdaEquality,  sqequalRule instantiate universeEquality because_Cache

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



Date html generated: 2016_10_21-AM-09_34_49
Last ObjectModification: 2016_07_12-AM-04_59_33

Theory : core_2


Home Index