Theorem mtoi 190

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 189	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  316  mtbiri  317  axc10  2252  ssdifsn  4318  pwnss  4830  eunex  4859  nsuceq0  5805  onssnel2i  5838  abnex  6965  ssonprc  6992  reldmtpos  7360  dmtpos  7364  tfrlem15  7488  tz7.44-2  7503  tz7.48-3  7539  2pwuninel  8115  2pwne  8116  nnsdomg  8219  r111  8638  r1pwss  8647  wfelirr  8688  rankxplim3  8744  carduni  8807  pr2ne  8828  alephle  8911  alephfp  8931  pwcdadom  9038  cfsuc  9079  fin23lem28  9162  fin23lem30  9164  isfin1-2  9207  ac5b  9300  zorn2lem4  9321  zorn2lem7  9324  cfpwsdom  9406  nd1  9409  nd2  9410  canthp1  9476  pwfseqlem1  9480  gchhar  9501  winalim2  9518  ltxrlt  10108  recgt0  10867  nnunb  11288  indstr  11756  wrdlen2i  13686  rlimno1  14384  lcmfnncl  15342  isprm2  15395  nprmdvds1  15418  divgcdodd  15422  coprm  15423  ramtcl2  15715  psgnunilem3  17916  torsubg  18257  prmcyg  18295  dprd2da  18441  prmirredlem  19841  pnfnei  21024  mnfnei  21025  1stccnp  21265  uzfbas  21702  ufinffr  21733  fin1aufil  21736  ovolunlem1a  23264  itg2gt0  23527  lgsquad2lem2  25110  dirith2  25217  umgrnloop0  26004  usgrnloop0ALT  26097  nfrgr2v  27136  hon0  28652  ifeqeqx  29361  dfon2lem7  31694  soseq  31751  noseponlem  31817  nosepssdm  31836  nodenselem8  31841  nolt02o  31845  bj-axc10v  32717  bj-eunex  32799  areacirclem4  33503  fdc  33541  dihglblem6  36629  pellexlem6  37398  pw2f1ocnv  37604  wepwsolem  37612  axc5c4c711toc5  38603  lptioo2  39863  lptioo1  39864  1neven  41932