Theorem mtoi 664

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 663	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 614  ax-in2 615

This theorem is referenced by:  mtbii  674  mtbiri  675  pwnss  4161  exmid1stab  4210  nsuceq0g  4420  abnex  4449  reg2exmidlema  4535  ordsuc  4564  onnmin  4569  ssnel  4570  ordtri2or2exmid  4572  ontri2orexmidim  4573  reg3exmidlemwe  4580  acexmidlemab  5871  reldmtpos  6256  dmtpos  6259  2pwuninelg  6286  onunsnss  6918  snon0  6937  nninfisol  7133  exmidomni  7142  pr2ne  7193  ltexprlemdisj  7607  recexprlemdisj  7631  caucvgprlemnkj  7667  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  caucvgprprlemnjltk  7692  inelr  8543  rimul  8544  recgt0  8809  zfz1iso  10823  isprm2  12119  nprmdvds1  12142  divgcdodd  12145  coprm  12146  coseq0q4123  14294  pwle2  14787  nninfalllem1  14796  nninfall  14797  nninfsellemqall  14803