Nuprl Lemma : and_true_l

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


Proof




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

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



Date html generated: 2019_06_20-AM-11_16_14
Last ObjectModification: 2018_09_26-AM-10_24_05

Theory : core_2


Home Index