Nuprl Lemma : band_commutes
∀[a,b:𝔹]. a ∧b b = b ∧b a
Proof
Definitions occuring in Statement :
band: p ∧b q,
bool: 𝔹,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
band: p ∧b q,
bfalse: ff,
ifthenelse: if b then t else f fi ,
prop: ℙ
Lemmas referenced :
equal-wf-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
unionElimination,
thin,
equalityElimination,
sqequalRule,
inlEquality,
axiomEquality,
natural_numberEquality,
extract_by_obid,
isectElimination,
intEquality,
baseClosed,
because_Cache,
hypothesis,
inrEquality,
isect_memberEquality,
hypothesisEquality
Latex:
\mforall{}[a,b:\mBbbB{}]. a \mwedge{}\msubb{} b = b \mwedge{}\msubb{} a
Date html generated:
2017_04_14-AM-07_29_43
Last ObjectModification:
2017_02_27-PM-02_58_11
Theory : bool_1
Home
Index