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  1948  pwnss  4478  eunex  4506  nsuceq0  4820  onssnel2i  4850  ssonprc  6424  reldmtpos  6774  dmtpos  6778  tfrlem15  6872  tz7.44-2  6884  tz7.48-3  6920  2pwuninel  7487  2pwne  7488  nnsdomg  7592  r111  8003  r1pwss  8012  wfelirr  8053  rankxplim3  8109  carduni  8172  pr2ne  8193  alephle  8279  alephfp  8299  pwcdadom  8406  cfsuc  8447  fin23lem28  8530  fin23lem30  8532  isfin1-2  8575  ac5b  8668  zorn2lem4  8689  zorn2lem7  8692  cfpwsdom  8769  nd1  8772  nd2  8773  canthp1  8842  pwfseqlem1  8846  gchhar  8867  winalim2  8884  ltxrlt  9466  recgt0  10194  nnunb  10596  indstr  10944  wrdlen2i  12567  rlimno1  13152  isprm2  13792  coprm  13807  nprmdvds1  13818  divgcdodd  13826  ramtcl2  14093  psgnunilem3  16023  torsubg  16357  prmcyg  16391  dprd2da  16563  prmirredlem  17939  prmirredlemOLD  17942  pnfnei  18846  mnfnei  18847  1stccnp  19088  uzfbas  19493  ufinffr  19524  fin1aufil  19527  ovolunlem1a  21001  itg2gt0  21260  lgsquad2lem2  22720  dirith2  22799  usgranloop0  23321  nbgranself2  23369  hon0  25219  ifeqeqx  25924  dfon2lem7  27624  soseq  27737  nodenselem3  27846  nodenselem8  27851  areacirclem4  28513  fdc  28667  pellexlem6  29201  pw2f1ocnv  29412  wepwsolem  29420  axc5c4c711toc5  29682  frgra2v  30617  bj-axc10v  32309  bj-eunex  32416  dihglblem6  35081