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

Theorem mtoi 202
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 201 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  329  mtbiri  330  sbn1  2111  axc10  2386  pwnss  5257  nsuceq0  6313  onssnel2i  6344  abnex  7563  ssonprc  7592  dmtpos  8003  tfrlem15  8151  tz7.44-2  8166  tz7.48-3  8203  2pwuninel  8826  2pwne  8827  nnsdomg  8959  r111  9420  r1pwss  9429  wfelirr  9470  rankxplim3  9526  carduni  9626  pr2ne  9648  alephle  9731  alephfp  9751  pwdjudom  9859  cfsuc  9900  fin23lem28  9983  fin23lem30  9985  isfin1-2  10028  ac5b  10121  zorn2lem4  10142  zorn2lem7  10145  cfpwsdom  10227  nd1  10230  nd2  10231  canthp1  10297  pwfseqlem1  10301  gchhar  10322  winalim2  10339  ltxrlt  10932  recgt0  11707  nnunb  12115  indstr  12541  wrdlen2i  14539  rlimno1  15249  lcmfnncl  16218  isprm2  16271  nprmdvds1  16295  divgcdodd  16299  coprm  16300  ramtcl2  16596  psgnunilem3  18920  torsubg  19271  prmcyg  19311  dprd2da  19461  prmirredlem  20491  pnfnei  22148  mnfnei  22149  1stccnp  22390  uzfbas  22826  ufinffr  22857  fin1aufil  22860  ovolunlem1a  24424  itg2gt0  24689  lgsquad2lem2  26297  dirith2  26440  umgrnloop0  27231  usgrnloop0ALT  27324  nfrgr2v  28386  hon0  29905  ifeqeqx  30635  dfon2lem7  33514  soseq  33573  noseponlem  33637  nosepssdm  33659  nodenselem8  33664  nolt02o  33668  nogt01o  33669  bj-axc10v  34745  sbn1ALT  34812  bj-nsnid  35011  areacirclem4  35641  fdc  35676  dihglblem6  39127  sn-inelr  40190  itrere  40191  retire  40192  pellexlem6  40406  pw2f1ocnv  40609  wepwsolem  40617  inaex  41635  axc5c4c711toc5  41740  lptioo2  42892  lptioo1  42893  1neven  45208
  Copyright terms: Public domain W3C validator