Theorem mtoi 636

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 635	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 586  ax-in2 587

This theorem is referenced by:  mtbii  646  mtbiri  647  pwnss  4043  nsuceq0g  4300  abnex  4328  reg2exmidlema  4409  ordsuc  4438  onnmin  4443  ssnel  4444  ordtri2or2exmid  4446  reg3exmidlemwe  4453  acexmidlemab  5722  reldmtpos  6104  dmtpos  6107  2pwuninelg  6134  onunsnss  6758  snon0  6776  exmidomni  6964  pr2ne  6998  ltexprlemdisj  7362  recexprlemdisj  7386  caucvgprlemnkj  7422  caucvgprprlemnkltj  7445  caucvgprprlemnkeqj  7446  caucvgprprlemnjltk  7447  inelr  8264  rimul  8265  recgt0  8518  zfz1iso  10477  isprm2  11644  nprmdvds1  11666  divgcdodd  11667  coprm  11668  pwle2  12885  exmid1stab  12887  nninfalllem1  12895  nninfall  12896  nninfsellemqall  12903