Nuprl Lemma : or_true_r

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


Proof




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

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



Date html generated: 2019_06_20-AM-11_16_26
Last ObjectModification: 2018_09_26-AM-10_24_13

Theory : core_2


Home Index