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

Theorem mtoi 188
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 187 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  314  mtbiri  315  axc10  2235  pwnss  4748  eunex  4777  nsuceq0  5705  onssnel2i  5738  ssonprc  6858  reldmtpos  7221  dmtpos  7225  tfrlem15  7349  tz7.44-2  7364  tz7.48-3  7400  2pwuninel  7974  2pwne  7975  nnsdomg  8078  r111  8495  r1pwss  8504  wfelirr  8545  rankxplim3  8601  carduni  8664  pr2ne  8685  alephle  8768  alephfp  8788  pwcdadom  8895  cfsuc  8936  fin23lem28  9019  fin23lem30  9021  isfin1-2  9064  ac5b  9157  zorn2lem4  9178  zorn2lem7  9181  cfpwsdom  9259  nd1  9262  nd2  9263  canthp1  9329  pwfseqlem1  9333  gchhar  9354  winalim2  9371  ltxrlt  9956  recgt0  10713  nnunb  11132  indstr  11585  wrdlen2i  13477  rlimno1  14175  lcmfnncl  15123  isprm2  15176  nprmdvds1  15199  divgcdodd  15203  coprm  15204  ramtcl2  15496  psgnunilem3  17682  torsubg  18023  prmcyg  18061  dprd2da  18207  prmirredlem  19602  pnfnei  20773  mnfnei  20774  1stccnp  21014  uzfbas  21451  ufinffr  21482  fin1aufil  21485  ovolunlem1a  22985  itg2gt0  23247  lgsquad2lem2  24824  dirith2  24931  usgranloop0  25672  nbgranself2  25728  frgra2v  26289  hon0  27839  ifeqeqx  28548  dfon2lem7  30741  soseq  30798  noseponlem  30868  nodenselem3  30885  nodenselem8  30890  bj-axc10v  31707  bj-eunex  31797  areacirclem4  32473  fdc  32511  dihglblem6  35447  pellexlem6  36216  pw2f1ocnv  36422  wepwsolem  36430  axc5c4c711toc5  37425  lptioo2  38499  lptioo1  38500  umgrnloop0  40333  usgrnloop0ALT  40431  nfrgr2v  41441  1neven  41721
  Copyright terms: Public domain W3C validator