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

Theorem mtoi 172
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 11 . 2  |-  ( ph  ->  -.  ch )
3 mtoi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mtod 171 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mtbii  295  mtbiri  296  spOLD  1765  equsalhwOLD  1862  ax9o  1955  dvelimvOLD  2029  pwnss  4367  eunex  4394  nsuceq0  4663  onssnel2i  4694  ssonprc  4774  reldmtpos  6489  dmtpos  6493  tfrlem15  6655  tz7.44-2  6667  tz7.48-3  6703  abianfp  6718  2pwuninel  7264  2pwne  7265  nnsdomg  7368  r111  7703  r1pwss  7712  wfelirr  7753  rankxplim3  7807  carduni  7870  pr2ne  7891  alephle  7971  alephfp  7991  pwcdadom  8098  cfsuc  8139  fin23lem28  8222  fin23lem30  8224  isfin1-2  8267  ac5b  8360  zorn2lem4  8381  zorn2lem7  8384  cfpwsdom  8461  nd1  8464  nd2  8465  canthp1  8531  pwfseqlem1  8535  gchhar  8548  winalim2  8573  ltxrlt  9148  recgt0  9856  nnunb  10219  indstr  10547  rlimno1  12449  isprm2  13089  coprm  13102  nprmdvds1  13113  divgcdodd  13121  ramtcl2  13381  torsubg  15471  prmcyg  15505  dprd2da  15602  prmirredlem  16775  pnfnei  17286  mnfnei  17287  1stccnp  17527  uzfbas  17932  ufinffr  17963  fin1aufil  17966  ovolunlem1a  19394  itg2gt0  19654  lgsquad2lem2  21145  dirith2  21224  usgranloop0  21402  nbgranself2  21450  hon0  23298  ifeqeqx  24003  dfon2lem7  25418  soseq  25531  nodenselem3  25640  nodenselem8  25645  areacirclem4  26297  fdc  26451  pellexlem6  26899  pw2f1ocnv  27110  wepwsolem  27118  psgnunilem3  27398  ax4567to4  27581  dvelimvNEW7  29524  ax9oNEW7  29531  dihglblem6  32200
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator