Theorem mtoi 665

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 9	. 2 |- ( ph -> -. ch )
3		mtoi.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	mtod 664	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-in1 615  ax-in2 616

This theorem is referenced by:  mtbii  675  mtbiri  676  pwnss  4188  exmid1stab  4237  nsuceq0g  4449  abnex  4478  reg2exmidlema  4566  ordsuc  4595  onnmin  4600  ssnel  4601  ordtri2or2exmid  4603  ontri2orexmidim  4604  reg3exmidlemwe  4611  acexmidlemab  5912  reldmtpos  6306  dmtpos  6309  2pwuninelg  6336  onunsnss  6973  snon0  6994  nninfisol  7192  exmidomni  7201  pr2ne  7252  ltexprlemdisj  7666  recexprlemdisj  7690  caucvgprlemnkj  7726  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnjltk  7751  inelr  8603  rimul  8604  recgt0  8869  zfz1iso  10912  isprm2  12255  nprmdvds1  12278  divgcdodd  12281  coprm  12282  coseq0q4123  14969  pwle2  15489  nninfalllem1  15498  nninfall  15499  nninfsellemqall  15505