Theorem mtoi 653

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 652	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 603  ax-in2 604

This theorem is referenced by:  mtbii  663  mtbiri  664  pwnss  4083  nsuceq0g  4340  abnex  4368  reg2exmidlema  4449  ordsuc  4478  onnmin  4483  ssnel  4484  ordtri2or2exmid  4486  reg3exmidlemwe  4493  acexmidlemab  5768  reldmtpos  6150  dmtpos  6153  2pwuninelg  6180  onunsnss  6805  snon0  6824  exmidomni  7014  pr2ne  7048  ltexprlemdisj  7414  recexprlemdisj  7438  caucvgprlemnkj  7474  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  inelr  8346  rimul  8347  recgt0  8608  zfz1iso  10584  isprm2  11798  nprmdvds1  11820  divgcdodd  11821  coprm  11822  coseq0q4123  12915  pwle2  13193  exmid1stab  13195  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211