Nuprl Lemma : implies_functionality_wrt_implies

[P1,P2,Q1,Q2:ℙ].  ({P1  P2}  {Q1  Q2}  {(P1  Q1)  P2  Q2})


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: guard: {T} rev_implies:  Q implies:  Q
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] implies:  Q member: t ∈ T prop: rev_implies:  Q
Lemmas referenced :  rev_implies_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  lambdaFormation hypothesisEquality functionEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis Error :inhabitedIsType,  Error :universeIsType,  universeEquality independent_functionElimination

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



Date html generated: 2019_06_20-AM-11_16_54
Last ObjectModification: 2018_09_26-AM-10_24_29

Theory : core_2


Home Index