Nuprl Lemma : and_false_l
∀[A:Top]. (False ∧ A ⇐⇒ False)
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
top: Top,
iff: P ⇐⇒ Q,
and: P ∧ Q,
false: False
Definitions unfolded in proof :
and: P ∧ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
false: False,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q
Lemmas referenced :
top_wf,
false_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
independent_pairFormation,
lambdaFormation,
cut,
hypothesis,
productEquality,
lemma_by_obid,
sqequalHypSubstitution,
voidElimination,
productElimination,
thin
Latex:
\mforall{}[A:Top]. (False \mwedge{} A \mLeftarrow{}{}\mRightarrow{} False)
Date html generated:
2016_05_13-PM-03_11_13
Last ObjectModification:
2016_01_06-PM-05_25_39
Theory : core_2
Home
Index