Theorem mtoi 182

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 181	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  304  mtbiri  305  axc10  2095  pwnss  4567  eunex  4595  nsuceq0  5502  onssnel2i  5532  ssonprc  6616  reldmtpos  6978  dmtpos  6982  tfrlem15  7107  tz7.44-2  7122  tz7.48-3  7158  2pwuninel  7724  2pwne  7725  nnsdomg  7827  r111  8243  r1pwss  8252  wfelirr  8293  rankxplim3  8349  carduni  8412  pr2ne  8433  alephle  8516  alephfp  8536  pwcdadom  8643  cfsuc  8684  fin23lem28  8767  fin23lem30  8769  isfin1-2  8812  ac5b  8905  zorn2lem4  8926  zorn2lem7  8929  cfpwsdom  9006  nd1  9009  nd2  9010  canthp1  9076  pwfseqlem1  9080  gchhar  9101  winalim2  9118  ltxrlt  9701  recgt0  10446  nnunb  10862  indstr  11224  wrdlen2i  13014  rlimno1  13710  lcmfnncl  14595  isprm2  14625  nprmdvds1  14643  divgcdodd  14646  coprm  14650  ramtcl2  14959  ramtcl2OLD  14960  psgnunilem3  17130  torsubg  17485  prmcyg  17521  dprd2da  17668  prmirredlem  19057  pnfnei  20229  mnfnei  20230  1stccnp  20470  uzfbas  20906  ufinffr  20937  fin1aufil  20940  ovolunlem1a  22442  itg2gt0  22711  lgsquad2lem2  24280  dirith2  24359  usgranloop0  25100  nbgranself2  25157  frgra2v  25720  hon0  27439  ifeqeqx  28151  dfon2lem7  30428  soseq  30485  noseponlem  30548  nodenselem3  30565  nodenselem8  30570  bj-axc10v  31311  bj-eunex  31407  areacirclem4  32028  fdc  32067  dihglblem6  34902  pellexlem6  35672  pw2f1ocnv  35886  wepwsolem  35894  axc5c4c711toc5  36747  lptioo2  37705  lptioo1  37706  umgrnloop0  39183  usgrnloop0ALT  39274  1neven  39919