(
Tr:(Term
Prop), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr))
t,e:Term. NOT(t)/e = NOT(t/e)t:Term. s(t) reps t/s(t)
(A 
B & C) (A C) B) (B C) (A C) P) False| Rank | Theorem | Name |
| 5 | Thm* (Tr:(TermProp), tr:Term, L:(TermProp). RepsTruth(L; Tr; tr)) | [Tarski] |
| cites | ||
| 0 | Thm* t,e:Term. NOT(t)/e = NOT(t/e) | [qnot_subx] |
| 4 | Thm* t:Term. s(t) reps 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] |