Nuprl Lemma : or_functionality_wrt_uiff3

[P1,P2,Q1,Q2:ℙ].  ((P1 P2 ∈ ℙ {uiff(Q1;Q2)}  {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})


Proof




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

Latex:
\mforall{}[P1,P2,Q1,Q2:\mBbbP{}].    ((P1  =  P2)  {}\mRightarrow{}  \{uiff(Q1;Q2)\}  {}\mRightarrow{}  \{P1  \mvee{}  Q1  \mLeftarrow{}{}\mRightarrow{}  P2  \mvee{}  Q2\})



Date html generated: 2019_06_20-AM-11_17_16
Last ObjectModification: 2018_09_26-AM-10_24_44

Theory : core_2


Home Index