Nuprl Lemma : minimal-example1-ext
∀[A,B,X:ℙ]. ((((A ⇒ B) ⇒ X) ⇒ X) ⇒ ((A ⇒ X) ⇒ X) ⇒ (B ⇒ X) ⇒ X)
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q
Definitions unfolded in proof :
minimal-example1,
member: t ∈ T
Lemmas referenced :
minimal-example1
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}[A,B,X:\mBbbP{}]. ((((A {}\mRightarrow{} B) {}\mRightarrow{} X) {}\mRightarrow{} X) {}\mRightarrow{} ((A {}\mRightarrow{} X) {}\mRightarrow{} X) {}\mRightarrow{} (B {}\mRightarrow{} X) {}\mRightarrow{} X)
Date html generated:
2017_09_29-PM-05_46_42
Last ObjectModification:
2017_09_23-PM-05_26_19
Theory : core_2
Home
Index