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  4159  exmid1stab  4208  nsuceq0g  4418  abnex  4447  reg2exmidlema  4533  ordsuc  4562  onnmin  4567  ssnel  4568  ordtri2or2exmid  4570  ontri2orexmidim  4571  reg3exmidlemwe  4578  acexmidlemab  5868  reldmtpos  6253  dmtpos  6256  2pwuninelg  6283  onunsnss  6915  snon0  6934  nninfisol  7130  exmidomni  7139  pr2ne  7190  ltexprlemdisj  7604  recexprlemdisj  7628  caucvgprlemnkj  7664  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemnjltk  7689  inelr  8539  rimul  8540  recgt0  8805  zfz1iso  10816  isprm2  12111  nprmdvds1  12134  divgcdodd  12137  coprm  12138  coseq0q4123  14186  pwle2  14668  nninfalllem1  14677  nninfall  14678  nninfsellemqall  14684