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  1988  pwnss  4598  eunex  4626  nsuceq0  4944  onssnel2i  4974  ssonprc  6608  reldmtpos  6961  dmtpos  6965  tfrlem15  7059  tz7.44-2  7071  tz7.48-3  7107  2pwuninel  7670  2pwne  7671  nnsdomg  7777  r111  8191  r1pwss  8200  wfelirr  8241  rankxplim3  8297  carduni  8360  pr2ne  8381  alephle  8467  alephfp  8487  pwcdadom  8594  cfsuc  8635  fin23lem28  8718  fin23lem30  8720  isfin1-2  8763  ac5b  8856  zorn2lem4  8877  zorn2lem7  8880  cfpwsdom  8957  nd1  8960  nd2  8961  canthp1  9030  pwfseqlem1  9034  gchhar  9055  winalim2  9072  ltxrlt  9653  recgt0  10387  nnunb  10792  indstr  11154  wrdlen2i  12858  rlimno1  13450  isprm2  14097  coprm  14113  nprmdvds1  14124  divgcdodd  14132  ramtcl2  14401  psgnunilem3  16390  torsubg  16729  prmcyg  16765  dprd2da  16959  prmirredlem  18390  prmirredlemOLD  18393  pnfnei  19587  mnfnei  19588  1stccnp  19829  uzfbas  20265  ufinffr  20296  fin1aufil  20299  ovolunlem1a  21773  itg2gt0  22033  lgsquad2lem2  23499  dirith2  23578  usgranloop0  24245  nbgranself2  24301  frgra2v  24864  hon0  26577  ifeqeqx  27284  dfon2lem7  29189  soseq  29302  nodenselem3  29411  nodenselem8  29416  areacirclem4  30078  fdc  30206  pellexlem6  30738  pw2f1ocnv  30947  wepwsolem  30955  axc5c4c711toc5  31256  lptioo2  31541  lptioo1  31542  1neven  32438  bj-axc10v  33991  bj-eunex  34097  dihglblem6  36769