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

Theorem mtoi 190
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 189 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  316  mtbiri  317  axc10  2250  ssdifsn  4309  pwnss  4821  eunex  4850  nsuceq0  5793  onssnel2i  5826  abnex  6950  ssonprc  6977  reldmtpos  7345  dmtpos  7349  tfrlem15  7473  tz7.44-2  7488  tz7.48-3  7524  2pwuninel  8100  2pwne  8101  nnsdomg  8204  r111  8623  r1pwss  8632  wfelirr  8673  rankxplim3  8729  carduni  8792  pr2ne  8813  alephle  8896  alephfp  8916  pwcdadom  9023  cfsuc  9064  fin23lem28  9147  fin23lem30  9149  isfin1-2  9192  ac5b  9285  zorn2lem4  9306  zorn2lem7  9309  cfpwsdom  9391  nd1  9394  nd2  9395  canthp1  9461  pwfseqlem1  9465  gchhar  9486  winalim2  9503  ltxrlt  10093  recgt0  10852  nnunb  11273  indstr  11741  wrdlen2i  13667  rlimno1  14365  lcmfnncl  15323  isprm2  15376  nprmdvds1  15399  divgcdodd  15403  coprm  15404  ramtcl2  15696  psgnunilem3  17897  torsubg  18238  prmcyg  18276  dprd2da  18422  prmirredlem  19822  pnfnei  21005  mnfnei  21006  1stccnp  21246  uzfbas  21683  ufinffr  21714  fin1aufil  21717  ovolunlem1a  23245  itg2gt0  23508  lgsquad2lem2  25091  dirith2  25198  umgrnloop0  25985  usgrnloop0ALT  26078  nfrgr2v  27116  hon0  28622  ifeqeqx  29333  dfon2lem7  31668  soseq  31725  noseponlem  31791  nosepssdm  31810  nodenselem8  31815  nolt02o  31819  bj-axc10v  32692  bj-eunex  32774  areacirclem4  33474  fdc  33512  dihglblem6  36448  pellexlem6  37217  pw2f1ocnv  37423  wepwsolem  37431  axc5c4c711toc5  38423  lptioo2  39663  lptioo1  39664  1neven  41697
  Copyright terms: Public domain W3C validator