(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: Tarski 1 1 1 2 1 1 1 1
1. Tr: TermProp
2. tr: Term
3. L: TermProp
4. S: Term
5. S = s(NOT(tr))
6. S reps NOT(tr/S)
7. Tr(tr/S) Tr(NOT(tr/S))
8. Tr(NOT(tr/S)) Tr(tr/S)
False
By:
FwdThru Thm* (A B) (B C) (A C) [7;8]
THEN
OnHyps [8;7] Thin
Generated subgoal:

17. Tr(tr/S) Tr(tr/S)
False		1 step

About:
applyfunctionequalpropimpliesfalse

(13steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc