Nuprl Lemma : not_over_or_a
∀[A,B:ℙ]. uiff(¬(A ∨ B);{(¬A) ∧ (¬B)})
Proof
Definitions occuring in Statement :
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
not: ¬A,
or: P ∨ Q,
and: P ∧ Q
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
not_over_or
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}[A,B:\mBbbP{}]. uiff(\mneg{}(A \mvee{} B);\{(\mneg{}A) \mwedge{} (\mneg{}B)\})
Date html generated:
2016_05_13-PM-03_10_58
Last ObjectModification:
2016_01_06-PM-05_26_09
Theory : core_2
Home
Index