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

Theorem mtoi 178
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 177 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  mtbii  302  mtbiri  303  axc10  2004  pwnss  4617  eunex  4645  nsuceq0  4963  onssnel2i  4993  ssonprc  6627  reldmtpos  6982  dmtpos  6986  tfrlem15  7080  tz7.44-2  7092  tz7.48-3  7128  2pwuninel  7692  2pwne  7693  nnsdomg  7799  r111  8214  r1pwss  8223  wfelirr  8264  rankxplim3  8320  carduni  8383  pr2ne  8404  alephle  8490  alephfp  8510  pwcdadom  8617  cfsuc  8658  fin23lem28  8741  fin23lem30  8743  isfin1-2  8786  ac5b  8879  zorn2lem4  8900  zorn2lem7  8903  cfpwsdom  8980  nd1  8983  nd2  8984  canthp1  9053  pwfseqlem1  9057  gchhar  9078  winalim2  9095  ltxrlt  9676  recgt0  10411  nnunb  10816  indstr  11179  wrdlen2i  12884  rlimno1  13476  isprm2  14225  coprm  14241  nprmdvds1  14252  divgcdodd  14260  ramtcl2  14529  psgnunilem3  16521  torsubg  16860  prmcyg  16896  dprd2da  17091  prmirredlem  18523  prmirredlemOLD  18526  pnfnei  19721  mnfnei  19722  1stccnp  19963  uzfbas  20399  ufinffr  20430  fin1aufil  20433  ovolunlem1a  21907  itg2gt0  22167  lgsquad2lem2  23634  dirith2  23713  usgranloop0  24380  nbgranself2  24436  frgra2v  24999  hon0  26712  ifeqeqx  27419  dfon2lem7  29221  soseq  29334  nodenselem3  29443  nodenselem8  29448  areacirclem4  30110  fdc  30238  pellexlem6  30770  pw2f1ocnv  30979  wepwsolem  30987  axc5c4c711toc5  31309  lptioo2  31637  lptioo1  31638  1neven  32738  bj-axc10v  34277  bj-eunex  34385  dihglblem6  37067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator