Nuprl Lemma : minimal-not-not-xmiddle-program

[P,A:ℙ].  (((P ∨ (P  A))  A)  A)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: implies:  Q or: P ∨ Q
Definitions unfolded in proof :  member: t ∈ T minimal-not-not-xmiddle
Lemmas referenced :  minimal-not-not-xmiddle
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[P,A:\mBbbP{}].    (((P  \mvee{}  (P  {}\mRightarrow{}  A))  {}\mRightarrow{}  A)  {}\mRightarrow{}  A)



Date html generated: 2017_09_29-PM-05_46_55
Last ObjectModification: 2017_09_19-PM-04_53_07

Theory : core_2


Home Index