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

Theorem mtoi 201
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 200 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  328  mtbiri  329  axc10  2399  pwnss  5249  nsuceq0  6270  onssnel2i  6300  abnex  7478  ssonprc  7506  dmtpos  7903  tfrlem15  8027  tz7.44-2  8042  tz7.48-3  8079  2pwuninel  8671  2pwne  8672  nnsdomg  8776  r111  9203  r1pwss  9212  wfelirr  9253  rankxplim3  9309  carduni  9409  pr2ne  9430  alephle  9513  alephfp  9533  pwdjudom  9637  cfsuc  9678  fin23lem28  9761  fin23lem30  9763  isfin1-2  9806  ac5b  9899  zorn2lem4  9920  zorn2lem7  9923  cfpwsdom  10005  nd1  10008  nd2  10009  canthp1  10075  pwfseqlem1  10079  gchhar  10100  winalim2  10117  ltxrlt  10710  recgt0  11485  nnunb  11892  indstr  12315  wrdlen2i  14303  rlimno1  15009  lcmfnncl  15972  isprm2  16025  nprmdvds1  16049  divgcdodd  16053  coprm  16054  ramtcl2  16346  psgnunilem3  18623  torsubg  18973  prmcyg  19013  dprd2da  19163  prmirredlem  20639  pnfnei  21827  mnfnei  21828  1stccnp  22069  uzfbas  22505  ufinffr  22536  fin1aufil  22539  ovolunlem1a  24096  itg2gt0  24360  lgsquad2lem2  25960  dirith2  26103  umgrnloop0  26893  usgrnloop0ALT  26986  nfrgr2v  28050  hon0  29569  ifeqeqx  30296  dfon2lem7  33034  soseq  33096  noseponlem  33171  nosepssdm  33190  nodenselem8  33195  nolt02o  33199  bj-axc10v  34115  bj-nsnid  34361  areacirclem4  34984  fdc  35019  dihglblem6  38475  sbn1  39103  pellexlem6  39431  pw2f1ocnv  39634  wepwsolem  39642  inaex  40633  axc5c4c711toc5  40734  lptioo2  41912  lptioo1  41913  1neven  44204
  Copyright terms: Public domain W3C validator