Nuprl Lemma : not-not-p-or-not-p-prgram
∀P,A:ℙ. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Proof
Definitions occuring in Statement :
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q
Definitions unfolded in proof :
member: t ∈ T,
not-not-p-or-not-p
Lemmas referenced :
not-not-p-or-not-p
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_44
Last ObjectModification:
2017_09_19-PM-04_50_08
Theory : core_2
Home
Index