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  1716  equsalhw  1730  dvelimv  1879  ax9o  1890  pwnss  4176  eunex  4203  nsuceq0  4472  onssnel2i  4503  ssonprc  4583  reldmtpos  6242  dmtpos  6246  tfrlem15  6408  tz7.44-2  6420  tz7.48-3  6456  abianfp  6471  2pwuninel  7016  2pwne  7017  nnsdomg  7116  r111  7447  r1pwss  7456  wfelirr  7497  rankxplim3  7551  carduni  7614  pr2ne  7635  alephle  7715  alephfp  7735  pwcdadom  7842  cfsuc  7883  fin23lem28  7966  fin23lem30  7968  isfin1-2  8011  ac5b  8105  zorn2lem4  8126  zorn2lem7  8129  cfpwsdom  8206  nd1  8209  nd2  8210  canthp1  8276  pwfseqlem1  8280  gchhar  8293  winalim2  8318  ltxrlt  8893  recgt0  9600  nnunb  9961  indstr  10287  rlimno1  12127  isprm2  12766  coprm  12779  nprmdvds1  12790  divgcdodd  12798  ramtcl2  13058  torsubg  15146  prmcyg  15180  dprd2da  15277  prmirredlem  16446  pnfnei  16950  mnfnei  16951  1stccnp  17188  uzfbas  17593  ufinffr  17624  fin1aufil  17627  ovolunlem1a  18855  itg2gt0  19115  lgsquad2lem2  20598  dirith2  20677  hon0  22373  ifeqeqx  23034  dfon2lem7  24145  soseq  24254  nodenselem3  24337  nodenselem8  24342  areacirclem5  24929  fdc  26455  pellexlem6  26919  pw2f1ocnv  27130  wepwsolem  27138  psgnunilem3  27419  ax4567to4  27602  nbgranself2  28151  ax10lem17ALT  29123  ax9lem3  29142  ax9lem4  29143  ax9lem17  29156  dihglblem6  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator