![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mto | Unicode version |
Description: The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Ref | Expression |
---|---|
mto.1 |
![]() ![]() ![]() |
mto.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mto |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mto.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mto.1 |
. . 3
![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | pm2.65i 629 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 604 ax-in2 605 |
This theorem is referenced by: mtbi 660 pm3.2ni 803 pm5.16 814 intnan 915 intnanr 916 equidqe 1513 nexr 1671 ru 2912 neldifsn 3661 nvel 4069 nlim0 4324 snnex 4377 onprc 4475 dtruex 4482 ordsoexmid 4485 nprrel 4592 0xp 4627 iprc 4815 son2lpi 4943 nfunv 5164 0fv 5464 acexmidlema 5773 acexmidlemb 5774 acexmidlemab 5776 mpo0 5849 php5dom 6765 fi0 6871 0nnq 7196 0npr 7315 1ne0sr 7598 pnfnre 7831 mnfnre 7832 ine0 8180 inelr 8370 nn0nepnf 9072 1nuz2 9427 0nrp 9506 inftonninf 10245 eirr 11521 odd2np1 11606 n2dvds1 11645 1nprm 11831 structcnvcnv 12014 fvsetsid 12032 0ntop 12213 topnex 12294 bj-nnst 13135 bj-nvel 13266 pwle2 13366 exmidsbthrlem 13392 trirec0xor 13413 |
Copyright terms: Public domain | W3C validator |