Theorem mtoi 181

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 180	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  303  mtbiri  304  axc10  2057  pwnss  4581  eunex  4609  nsuceq0  5513  onssnel2i  5543  ssonprc  6624  reldmtpos  6980  dmtpos  6984  tfrlem15  7109  tz7.44-2  7124  tz7.48-3  7160  2pwuninel  7724  2pwne  7725  nnsdomg  7827  r111  8236  r1pwss  8245  wfelirr  8286  rankxplim3  8342  carduni  8405  pr2ne  8426  alephle  8508  alephfp  8528  pwcdadom  8635  cfsuc  8676  fin23lem28  8759  fin23lem30  8761  isfin1-2  8804  ac5b  8897  zorn2lem4  8918  zorn2lem7  8921  cfpwsdom  8998  nd1  9001  nd2  9002  canthp1  9068  pwfseqlem1  9072  gchhar  9093  winalim2  9110  ltxrlt  9693  recgt0  10438  nnunb  10854  indstr  11216  wrdlen2i  12989  rlimno1  13684  lcmfnncl  14562  isprm2  14592  nprmdvds1  14610  divgcdodd  14613  coprm  14617  ramtcl2  14926  ramtcl2OLD  14927  psgnunilem3  17089  torsubg  17433  prmcyg  17469  dprd2da  17616  prmirredlem  19001  pnfnei  20173  mnfnei  20174  1stccnp  20414  uzfbas  20850  ufinffr  20881  fin1aufil  20884  ovolunlem1a  22356  itg2gt0  22625  lgsquad2lem2  24189  dirith2  24268  usgranloop0  24994  nbgranself2  25050  frgra2v  25613  hon0  27322  ifeqeqx  28038  dfon2lem7  30263  soseq  30320  nodenselem3  30398  nodenselem8  30403  bj-axc10v  31098  bj-eunex  31206  areacirclem4  31783  fdc  31822  dihglblem6  34661  pellexlem6  35432  pw2f1ocnv  35646  wepwsolem  35654  axc5c4c711toc5  36438  lptioo2  37331  lptioo1  37332  1neven  38747