![]() |
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 326 mtbiri 327 sbn1 2106 axc10 2384 pwnss 5311 nsuceq0 6405 onssnel2i 6439 abnex 7696 ssonprc 7727 soseq 8096 dmtpos 8174 tfrlem15 8343 tz7.44-2 8358 tz7.48-3 8395 2pwuninel 9083 2pwne 9084 nnsdomg 9253 nnsdomgOLD 9254 r111 9718 r1pwss 9727 wfelirr 9768 rankxplim3 9824 carduni 9924 pr2neOLD 9948 alephle 10031 alephfp 10051 pwdjudom 10159 cfsuc 10200 fin23lem28 10283 fin23lem30 10285 isfin1-2 10328 ac5b 10421 zorn2lem4 10442 zorn2lem7 10445 cfpwsdom 10527 nd1 10530 nd2 10531 canthp1 10597 pwfseqlem1 10601 gchhar 10622 winalim2 10639 ltxrlt 11232 recgt0 12008 nnunb 12416 indstr 12848 wrdlen2i 14838 rlimno1 15545 lcmfnncl 16512 isprm2 16565 nprmdvds1 16589 divgcdodd 16593 coprm 16594 ramtcl2 16890 psgnunilem3 19285 torsubg 19639 prmcyg 19678 dprd2da 19828 prmirredlem 20909 pnfnei 22587 mnfnei 22588 1stccnp 22829 uzfbas 23265 ufinffr 23296 fin1aufil 23299 ovolunlem1a 24876 itg2gt0 25141 lgsquad2lem2 26749 dirith2 26892 noseponlem 27028 nosepssdm 27050 nodenselem8 27055 nolt02o 27059 nogt01o 27060 umgrnloop0 28102 usgrnloop0ALT 28195 nfrgr2v 29258 hon0 30777 ifeqeqx 31506 dfon2lem7 34403 bj-axc10v 35287 sbn1ALT 35353 bj-nsnid 35570 areacirclem4 36198 fdc 36233 dihglblem6 39832 sn-inelr 40963 itrere 40964 retire 40965 pellexlem6 41186 pw2f1ocnv 41390 wepwsolem 41398 inaex 42651 axc5c4c711toc5 42756 lptioo2 43946 lptioo1 43947 1neven 46304 |
Copyright terms: Public domain | W3C validator |