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	|- -. ch
mtoi.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mtoi	|- ( ph -> -. ps )

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 |- -. ch
2	1	a1i 11	. 2 |- ( ph -> -. ch )
3		mtoi.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	mtod 177	1 |- ( ph -> -. ps )

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  302  mtbiri  303  axc10  1947  pwnss  4445  eunex  4473  nsuceq0  4786  onssnel2i  4816  ssonprc  6392  reldmtpos  6742  dmtpos  6746  tfrlem15  6837  tz7.44-2  6849  tz7.48-3  6885  abianfp  6900  2pwuninel  7454  2pwne  7455  nnsdomg  7559  r111  7970  r1pwss  7979  wfelirr  8020  rankxplim3  8076  carduni  8139  pr2ne  8160  alephle  8246  alephfp  8266  pwcdadom  8373  cfsuc  8414  fin23lem28  8497  fin23lem30  8499  isfin1-2  8542  ac5b  8635  zorn2lem4  8656  zorn2lem7  8659  cfpwsdom  8736  nd1  8739  nd2  8740  canthp1  8808  pwfseqlem1  8812  gchhar  8833  winalim2  8850  ltxrlt  9432  recgt0  10160  nnunb  10562  indstr  10910  wrdlen2i  12529  rlimno1  13114  isprm2  13753  coprm  13768  nprmdvds1  13779  divgcdodd  13787  ramtcl2  14054  psgnunilem3  15981  torsubg  16315  prmcyg  16349  dprd2da  16514  prmirredlem  17758  prmirredlemOLD  17761  pnfnei  18665  mnfnei  18666  1stccnp  18907  uzfbas  19312  ufinffr  19343  fin1aufil  19346  ovolunlem1a  20820  itg2gt0  21079  lgsquad2lem2  22582  dirith2  22661  usgranloop0  23121  nbgranself2  23169  hon0  25019  ifeqeqx  25725  dfon2lem7  27448  soseq  27561  nodenselem3  27670  nodenselem8  27675  areacirclem4  28328  fdc  28482  pellexlem6  29017  pw2f1ocnv  29228  wepwsolem  29236  axc5c4c711toc5  29498  frgra2v  30434  bj-axc10v  31841  bj-eunex  31937  dihglblem6  34555