ElisTarskiPf A Sections NuprlLIB Doc

RankTheoremName
5 Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))[Tarski]
cites
0 Thm* t,e:Term. SUBX(NOT(t); e) = NOT(SUBX(t; e))[qnot_subx]
4 Thm* t:Term. s(t) = SUBX(t; s(t))[s_reps]
0 Thm* B (A B & C) (A C)[prop_and_iff]
0 Thm* (A B) (B C) (A C)[prop_iff_trans]
0 Thm* (P P) False[prop_iff_contra]

ElisTarskiPf A Sections NuprlLIB Doc