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 199 | 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 327 mtbiri 328 axc10 2394 pwnss 5241 nsuceq0 6264 onssnel2i 6294 abnex 7468 ssonprc 7496 dmtpos 7893 tfrlem15 8017 tz7.44-2 8032 tz7.48-3 8069 2pwuninel 8660 2pwne 8661 nnsdomg 8765 r111 9192 r1pwss 9201 wfelirr 9242 rankxplim3 9298 carduni 9398 pr2ne 9419 alephle 9502 alephfp 9522 pwdjudom 9626 cfsuc 9667 fin23lem28 9750 fin23lem30 9752 isfin1-2 9795 ac5b 9888 zorn2lem4 9909 zorn2lem7 9912 cfpwsdom 9994 nd1 9997 nd2 9998 canthp1 10064 pwfseqlem1 10068 gchhar 10089 winalim2 10106 ltxrlt 10699 recgt0 11474 nnunb 11881 indstr 12304 wrdlen2i 14292 rlimno1 14998 lcmfnncl 15961 isprm2 16014 nprmdvds1 16038 divgcdodd 16042 coprm 16043 ramtcl2 16335 psgnunilem3 18553 torsubg 18903 prmcyg 18943 dprd2da 19093 prmirredlem 20568 pnfnei 21756 mnfnei 21757 1stccnp 21998 uzfbas 22434 ufinffr 22465 fin1aufil 22468 ovolunlem1a 24024 itg2gt0 24288 lgsquad2lem2 25888 dirith2 26031 umgrnloop0 26821 usgrnloop0ALT 26914 nfrgr2v 27978 hon0 29497 ifeqeqx 30224 dfon2lem7 32931 soseq 32993 noseponlem 33068 nosepssdm 33087 nodenselem8 33092 nolt02o 33096 bj-axc10v 34012 bj-nsnid 34256 areacirclem4 34866 fdc 34901 dihglblem6 38356 sbn1 38981 pellexlem6 39309 pw2f1ocnv 39512 wepwsolem 39520 inaex 40510 axc5c4c711toc5 40611 lptioo2 41788 lptioo1 41789 1neven 44131 |
Copyright terms: Public domain | W3C validator |