![]() |
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 197 | 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 325 mtbiri 326 sbn1 2097 axc10 2378 pwnss 5351 nsuceq0 6454 onssnel2i 6488 abnex 7760 ssonprc 7791 soseq 8164 dmtpos 8244 tfrlem15 8413 tz7.44-2 8428 tz7.48-3 8465 2pwuninel 9157 2pwne 9158 nnsdomg 9327 nnsdomgOLD 9328 r111 9800 r1pwss 9809 wfelirr 9850 rankxplim3 9906 carduni 10006 pr2neOLD 10030 alephle 10113 alephfp 10133 pwdjudom 10241 cfsuc 10282 fin23lem28 10365 fin23lem30 10367 isfin1-2 10410 ac5b 10503 zorn2lem4 10524 zorn2lem7 10527 cfpwsdom 10609 nd1 10612 nd2 10613 canthp1 10679 pwfseqlem1 10683 gchhar 10704 winalim2 10721 ltxrlt 11316 recgt0 12093 nnunb 12501 indstr 12933 wrdlen2i 14929 rlimno1 15636 lcmfnncl 16603 isprm2 16656 nprmdvds1 16680 divgcdodd 16684 coprm 16685 ramtcl2 16983 psgnunilem3 19463 torsubg 19821 prmcyg 19861 dprd2da 20011 prmirredlem 21415 pnfnei 23168 mnfnei 23169 1stccnp 23410 uzfbas 23846 ufinffr 23877 fin1aufil 23880 ovolunlem1a 25469 itg2gt0 25734 lgsquad2lem2 27363 dirith2 27506 noseponlem 27643 nosepssdm 27665 nodenselem8 27670 nolt02o 27674 nogt01o 27675 umgrnloop0 28994 usgrnloop0ALT 29090 nfrgr2v 30154 hon0 31675 ifeqeqx 32412 dfon2lem7 35516 bj-axc10v 36401 sbn1ALT 36466 bj-nsnid 36680 areacirclem4 37315 fdc 37349 dihglblem6 40943 itrere 42014 sn-inelr 42155 sn-itrere 42156 sn-retire 42157 pellexlem6 42396 pw2f1ocnv 42600 wepwsolem 42608 inaex 43876 axc5c4c711toc5 43981 lptioo2 45157 lptioo1 45158 1neven 47486 |
Copyright terms: Public domain | W3C validator |