Nuprl Lemma : minimal-triple-neg-ext

[E:Type]. ∀[A:ℙ].  (((A  E)  E)  ⇐⇒  E)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: iff: ⇐⇒ Q implies:  Q universe: Type
Definitions unfolded in proof :  member: t ∈ T minimal-triple-neg
Lemmas referenced :  minimal-triple-neg
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[E:Type].  \mforall{}[A:\mBbbP{}].    (((A  {}\mRightarrow{}  E)  {}\mRightarrow{}  E)  {}\mRightarrow{}  E  \mLeftarrow{}{}\mRightarrow{}  A  {}\mRightarrow{}  E)



Date html generated: 2018_05_21-PM-00_00_29
Last ObjectModification: 2018_05_19-AM-07_14_11

Theory : core_2


Home Index