Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mtoi | Structured version Visualization version GIF version |
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Ref | Expression |
---|---|
mtoi.1 | ⊢ ¬ 𝜒 |
mtoi.2 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
mtoi | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtoi.1 | . . 3 ⊢ ¬ 𝜒 | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜑 → ¬ 𝜒) |
3 | mtoi.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | mtod 201 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: mtbii 329 mtbiri 330 sbn1 2111 axc10 2386 pwnss 5257 nsuceq0 6313 onssnel2i 6344 abnex 7563 ssonprc 7592 dmtpos 8003 tfrlem15 8151 tz7.44-2 8166 tz7.48-3 8203 2pwuninel 8826 2pwne 8827 nnsdomg 8959 r111 9420 r1pwss 9429 wfelirr 9470 rankxplim3 9526 carduni 9626 pr2ne 9648 alephle 9731 alephfp 9751 pwdjudom 9859 cfsuc 9900 fin23lem28 9983 fin23lem30 9985 isfin1-2 10028 ac5b 10121 zorn2lem4 10142 zorn2lem7 10145 cfpwsdom 10227 nd1 10230 nd2 10231 canthp1 10297 pwfseqlem1 10301 gchhar 10322 winalim2 10339 ltxrlt 10932 recgt0 11707 nnunb 12115 indstr 12541 wrdlen2i 14539 rlimno1 15249 lcmfnncl 16218 isprm2 16271 nprmdvds1 16295 divgcdodd 16299 coprm 16300 ramtcl2 16596 psgnunilem3 18920 torsubg 19271 prmcyg 19311 dprd2da 19461 prmirredlem 20491 pnfnei 22148 mnfnei 22149 1stccnp 22390 uzfbas 22826 ufinffr 22857 fin1aufil 22860 ovolunlem1a 24424 itg2gt0 24689 lgsquad2lem2 26297 dirith2 26440 umgrnloop0 27231 usgrnloop0ALT 27324 nfrgr2v 28386 hon0 29905 ifeqeqx 30635 dfon2lem7 33514 soseq 33573 noseponlem 33637 nosepssdm 33659 nodenselem8 33664 nolt02o 33668 nogt01o 33669 bj-axc10v 34745 sbn1ALT 34812 bj-nsnid 35011 areacirclem4 35641 fdc 35676 dihglblem6 39127 sn-inelr 40190 itrere 40191 retire 40192 pellexlem6 40406 pw2f1ocnv 40609 wepwsolem 40617 inaex 41635 axc5c4c711toc5 41740 lptioo2 42892 lptioo1 42893 1neven 45208 |
Copyright terms: Public domain | W3C validator |