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 613 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 588 ax-in2 589 |
This theorem is referenced by: mtbi 644 pm3.2ni 787 pm5.16 798 intnan 899 intnanr 900 equidqe 1497 nexr 1655 ru 2881 neldifsn 3623 nvel 4031 nlim0 4286 snnex 4339 onprc 4437 dtruex 4444 ordsoexmid 4447 nprrel 4554 0xp 4589 iprc 4777 son2lpi 4905 nfunv 5126 0fv 5424 acexmidlema 5733 acexmidlemb 5734 acexmidlemab 5736 mpo0 5809 php5dom 6725 fi0 6831 0nnq 7140 0npr 7259 1ne0sr 7542 pnfnre 7775 mnfnre 7776 ine0 8124 inelr 8314 nn0nepnf 9016 1nuz2 9368 0nrp 9445 inftonninf 10182 eirr 11412 odd2np1 11497 n2dvds1 11536 1nprm 11722 structcnvcnv 11902 fvsetsid 11920 0ntop 12101 topnex 12182 bj-nnst 12891 bj-nvel 13022 pwle2 13120 exmidsbthrlem 13144 |
Copyright terms: Public domain | W3C validator |