Nuprl Lemma : and_false_r

[A:ℙ]. (A ∧ False ⇐⇒ False)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: iff: ⇐⇒ Q and: P ∧ Q false: False
Definitions unfolded in proof :  uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q false: False member: t ∈ T prop: rev_implies:  Q
Lemmas referenced :  false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  independent_pairFormation lambdaFormation cut sqequalHypSubstitution productElimination thin voidElimination hypothesis productEquality cumulativity hypothesisEquality introduction extract_by_obid Error :universeIsType,  universeEquality

Latex:
\mforall{}[A:\mBbbP{}].  (A  \mwedge{}  False  \mLeftarrow{}{}\mRightarrow{}  False)



Date html generated: 2019_06_20-AM-11_16_11
Last ObjectModification: 2018_09_26-AM-10_24_03

Theory : core_2


Home Index