Nuprl Lemma : not-not-1-xmiddle
∀[P:ℙ]. (¬¬(P ∨ (¬P)))
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
not: ¬A,
or: P ∨ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
not: ¬A,
prop: ℙ
Lemmas referenced :
minimal-not-not-xmiddle,
false_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
universeIsType,
universeEquality
Latex:
\mforall{}[P:\mBbbP{}]. (\mneg{}\mneg{}(P \mvee{} (\mneg{}P)))
Date html generated:
2020_05_19-PM-09_35_05
Last ObjectModification:
2019_10_17-PM-02_45_32
Theory : core_2
Home
Index