MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtoi Structured version   Visualization version   GIF version

Theorem mtoi 198
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1 ¬ 𝜒
mtoi.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtoi (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3 ¬ 𝜒
21a1i 11 . 2 (𝜑 → ¬ 𝜒)
3 mtoi.2 . 2 (𝜑 → (𝜓𝜒))
42, 3mtod 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