![]() |
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 190 | 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 318 mtbiri 319 axc10 2405 ssdifsnOLD 4537 pwnss 5051 eunexOLD 5089 nsuceq0 6042 onssnel2i 6072 abnex 7225 ssonprc 7252 reldmtpos 7624 dmtpos 7628 tfrlem15 7753 tz7.44-2 7768 tz7.48-3 7804 2pwuninel 8383 2pwne 8384 nnsdomg 8487 r111 8914 r1pwss 8923 wfelirr 8964 rankxplim3 9020 carduni 9119 pr2ne 9140 alephle 9223 alephfp 9243 pwcdadom 9352 cfsuc 9393 fin23lem28 9476 fin23lem30 9478 isfin1-2 9521 ac5b 9614 zorn2lem4 9635 zorn2lem7 9638 cfpwsdom 9720 nd1 9723 nd2 9724 canthp1 9790 pwfseqlem1 9794 gchhar 9815 winalim2 9832 ltxrlt 10426 recgt0 11196 nnunb 11613 indstr 12038 wrdlen2i 14062 rlimno1 14760 lcmfnncl 15714 isprm2 15766 nprmdvds1 15788 divgcdodd 15792 coprm 15793 ramtcl2 16085 psgnunilem3 18266 torsubg 18609 prmcyg 18647 dprd2da 18794 prmirredlem 20200 pnfnei 21394 mnfnei 21395 1stccnp 21635 uzfbas 22071 ufinffr 22102 fin1aufil 22105 ovolunlem1a 23661 itg2gt0 23925 lgsquad2lem2 25522 dirith2 25629 umgrnloop0 26406 usgrnloop0ALT 26500 nfrgr2v 27652 hon0 29206 ifeqeqx 29908 dfon2lem7 32231 soseq 32292 noseponlem 32355 nosepssdm 32374 nodenselem8 32379 nolt02o 32383 bj-axc10v 33250 bj-nsnid 33630 areacirclem4 34045 fdc 34082 dihglblem6 37414 pellexlem6 38241 pw2f1ocnv 38446 wepwsolem 38454 axc5c4c711toc5 39441 lptioo2 40657 lptioo1 40658 1neven 42778 |
Copyright terms: Public domain | W3C validator |