Nuprl Lemma : example2-ext

[A,B,C:Type].  (((A  B)  A)  (B  C)  (A  B)  (¬¬C))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] not: ¬A implies:  Q universe: Type
Definitions unfolded in proof :  member: t ∈ T example2
Lemmas referenced :  example2
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A,B,C:Type].    (((A  {}\mRightarrow{}  B)  {}\mRightarrow{}  A)  {}\mRightarrow{}  (B  {}\mRightarrow{}  C)  {}\mRightarrow{}  (A  {}\mRightarrow{}  B)  {}\mRightarrow{}  (\mneg{}\mneg{}C))



Date html generated: 2018_05_21-PM-08_55_11
Last ObjectModification: 2018_05_19-PM-05_07_34

Theory : general


Home Index