Nuprl Lemma : minimal-example1
∀[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 :
prop: ℙ,
member: t ∈ T,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x]
Rules used in proof :
universeEquality,
hypothesisEquality,
functionEquality,
thin,
independent_functionElimination,
sqequalHypSubstitution,
hypothesis,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
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_40
Last ObjectModification:
2017_09_23-PM-06_50_08
Theory : core_2
Home
Index