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

Theorem mtoi 169
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1  |-  -.  ch
mtoi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mtoi  |-  ( ph  ->  -.  ps )

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3  |-  -.  ch
21a1i 10 . 2  |-  ( ph  ->  -.  ch )
3 mtoi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mtod 168 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mtbii  293  mtbiri  294  sp  1728  equsalhw  1742  dvelimv  1892  ax9o  1903  pwnss  4192  eunex  4219  nsuceq0  4488  onssnel2i  4519  ssonprc  4599  reldmtpos  6258  dmtpos  6262  tfrlem15  6424  tz7.44-2  6436  tz7.48-3  6472  abianfp  6487  2pwuninel  7032  2pwne  7033  nnsdomg  7132  r111  7463  r1pwss  7472  wfelirr  7513  rankxplim3  7567  carduni  7630  pr2ne  7651  alephle  7731  alephfp  7751  pwcdadom  7858  cfsuc  7899  fin23lem28  7982  fin23lem30  7984  isfin1-2  8027  ac5b  8121  zorn2lem4  8142  zorn2lem7  8145  cfpwsdom  8222  nd1  8225  nd2  8226  canthp1  8292  pwfseqlem1  8296  gchhar  8309  winalim2  8334  ltxrlt  8909  recgt0  9616  nnunb  9977  indstr  10303  rlimno1  12143  isprm2  12782  coprm  12795  nprmdvds1  12806  divgcdodd  12814  ramtcl2  13074  torsubg  15162  prmcyg  15196  dprd2da  15293  prmirredlem  16462  pnfnei  16966  mnfnei  16967  1stccnp  17204  uzfbas  17609  ufinffr  17640  fin1aufil  17643  ovolunlem1a  18871  itg2gt0  19131  lgsquad2lem2  20614  dirith2  20693  hon0  22389  ifeqeqx  23050  dfon2lem7  24216  soseq  24325  nodenselem3  24408  nodenselem8  24413  areacirclem5  25032  fdc  26558  pellexlem6  27022  pw2f1ocnv  27233  wepwsolem  27241  psgnunilem3  27522  ax4567to4  27705  nbgranself2  28285  dvelimvNEW7  29439  ax9oNEW7  29446  ax10lem17ALT  29745  ax9lem3  29764  ax9lem4  29765  ax9lem17  29778  dihglblem6  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator