| 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 198 | 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 326 mtbiri 327 sbn1 2107 axc10 2390 pwnss 5352 nsuceq0 6467 onssnel2i 6501 abnex 7777 ssonprc 7807 soseq 8184 dmtpos 8263 tfrlem15 8432 tz7.44-2 8447 tz7.48-3 8484 2pwuninel 9172 2pwne 9173 nnsdomg 9335 nnsdomgOLD 9336 r111 9815 r1pwss 9824 wfelirr 9865 rankxplim3 9921 carduni 10021 pr2neOLD 10045 alephle 10128 alephfp 10148 pwdjudom 10255 cfsuc 10297 fin23lem28 10380 fin23lem30 10382 isfin1-2 10425 ac5b 10518 zorn2lem4 10539 zorn2lem7 10542 cfpwsdom 10624 nd1 10627 nd2 10628 canthp1 10694 pwfseqlem1 10698 gchhar 10719 winalim2 10736 ltxrlt 11331 recgt0 12113 nnunb 12522 indstr 12958 wrdlen2i 14981 rlimno1 15690 lcmfnncl 16666 isprm2 16719 nprmdvds1 16743 divgcdodd 16747 coprm 16748 ramtcl2 17049 psgnunilem3 19514 torsubg 19872 prmcyg 19912 dprd2da 20062 prmirredlem 21483 pnfnei 23228 mnfnei 23229 1stccnp 23470 uzfbas 23906 ufinffr 23937 fin1aufil 23940 ovolunlem1a 25531 itg2gt0 25795 lgsquad2lem2 27429 dirith2 27572 noseponlem 27709 nosepssdm 27731 nodenselem8 27736 nolt02o 27740 nogt01o 27741 umgrnloop0 29126 usgrnloop0ALT 29222 nfrgr2v 30291 hon0 31812 ifeqeqx 32555 axsepg2ALT 35097 dfon2lem7 35790 bj-axc10v 36794 sbn1ALT 36859 bj-nsnid 37071 areacirclem4 37718 fdc 37752 dihglblem6 41342 itrere 42353 sn-inelr 42497 sn-itrere 42498 sn-retire 42499 pellexlem6 42845 pw2f1ocnv 43049 wepwsolem 43054 inaex 44316 axc5c4c711toc5 44421 lptioo2 45646 lptioo1 45647 1neven 48154 |
| Copyright terms: Public domain | W3C validator |