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

Theorem mtoi 200
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 199 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  327  mtbiri  328  axc10  2394  pwnss  5241  nsuceq0  6264  onssnel2i  6294  abnex  7468  ssonprc  7496  dmtpos  7893  tfrlem15  8017  tz7.44-2  8032  tz7.48-3  8069  2pwuninel  8660  2pwne  8661  nnsdomg  8765  r111  9192  r1pwss  9201  wfelirr  9242  rankxplim3  9298  carduni  9398  pr2ne  9419  alephle  9502  alephfp  9522  pwdjudom  9626  cfsuc  9667  fin23lem28  9750  fin23lem30  9752  isfin1-2  9795  ac5b  9888  zorn2lem4  9909  zorn2lem7  9912  cfpwsdom  9994  nd1  9997  nd2  9998  canthp1  10064  pwfseqlem1  10068  gchhar  10089  winalim2  10106  ltxrlt  10699  recgt0  11474  nnunb  11881  indstr  12304  wrdlen2i  14292  rlimno1  14998  lcmfnncl  15961  isprm2  16014  nprmdvds1  16038  divgcdodd  16042  coprm  16043  ramtcl2  16335  psgnunilem3  18553  torsubg  18903  prmcyg  18943  dprd2da  19093  prmirredlem  20568  pnfnei  21756  mnfnei  21757  1stccnp  21998  uzfbas  22434  ufinffr  22465  fin1aufil  22468  ovolunlem1a  24024  itg2gt0  24288  lgsquad2lem2  25888  dirith2  26031  umgrnloop0  26821  usgrnloop0ALT  26914  nfrgr2v  27978  hon0  29497  ifeqeqx  30224  dfon2lem7  32931  soseq  32993  noseponlem  33068  nosepssdm  33087  nodenselem8  33092  nolt02o  33096  bj-axc10v  34012  bj-nsnid  34256  areacirclem4  34866  fdc  34901  dihglblem6  38356  sbn1  38981  pellexlem6  39309  pw2f1ocnv  39512  wepwsolem  39520  inaex  40510  axc5c4c711toc5  40611  lptioo2  41788  lptioo1  41789  1neven  44131
  Copyright terms: Public domain W3C validator