Nuprl Lemma : fRuleandI_wf
andI ∈ FOLRule()
Proof
Definitions occuring in Statement : 
fRuleandI: andI
, 
FOLRule: FOLRule()
, 
member: t ∈ T
Definitions unfolded in proof : 
member: t ∈ T
, 
FOLRule: FOLRule()
, 
fRuleandI: andI
, 
eq_atom: x =a y
, 
ifthenelse: if b then t else f fi 
, 
btrue: tt
, 
uall: ∀[x:A]. B[x]
Lemmas referenced : 
it_wf, 
ifthenelse_wf, 
eq_atom_wf, 
unit_wf2, 
bool_wf, 
nat_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
cut, 
sqequalRule, 
dependent_pairEquality_alt, 
tokenEquality, 
introduction, 
extract_by_obid, 
hypothesis, 
universeIsType, 
thin, 
instantiate, 
sqequalHypSubstitution, 
isectElimination, 
hypothesisEquality, 
universeEquality, 
intEquality, 
productEquality, 
voidEquality
Latex:
andI  \mmember{}  FOLRule()
Date html generated:
2020_05_20-AM-09_09_23
Last ObjectModification:
2020_01_22-PM-05_22_33
Theory : minimal-first-order-logic
Home
Index