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  1973  pwnss  4612  eunex  4640  nsuceq0  4958  onssnel2i  4988  ssonprc  6611  reldmtpos  6963  dmtpos  6967  tfrlem15  7061  tz7.44-2  7073  tz7.48-3  7109  2pwuninel  7672  2pwne  7673  nnsdomg  7779  r111  8193  r1pwss  8202  wfelirr  8243  rankxplim3  8299  carduni  8362  pr2ne  8383  alephle  8469  alephfp  8489  pwcdadom  8596  cfsuc  8637  fin23lem28  8720  fin23lem30  8722  isfin1-2  8765  ac5b  8858  zorn2lem4  8879  zorn2lem7  8882  cfpwsdom  8959  nd1  8962  nd2  8963  canthp1  9032  pwfseqlem1  9036  gchhar  9057  winalim2  9074  ltxrlt  9655  recgt0  10386  nnunb  10791  indstr  11150  wrdlen2i  12847  rlimno1  13439  isprm2  14084  coprm  14100  nprmdvds1  14111  divgcdodd  14119  ramtcl2  14388  psgnunilem3  16327  torsubg  16663  prmcyg  16699  dprd2da  16893  prmirredlem  18318  prmirredlemOLD  18321  pnfnei  19515  mnfnei  19516  1stccnp  19757  uzfbas  20162  ufinffr  20193  fin1aufil  20196  ovolunlem1a  21670  itg2gt0  21930  lgsquad2lem2  23390  dirith2  23469  usgranloop0  24084  nbgranself2  24140  frgra2v  24703  hon0  26416  ifeqeqx  27121  dfon2lem7  28826  soseq  28939  nodenselem3  29048  nodenselem8  29053  areacirclem4  29715  fdc  29869  pellexlem6  30402  pw2f1ocnv  30611  wepwsolem  30619  axc5c4c711toc5  30915  bj-axc10v  33377  bj-eunex  33484  dihglblem6  36155