Theorem mtoi 659

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 658	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 609  ax-in2 610

This theorem is referenced by:  mtbii  669  mtbiri  670  pwnss  4145  nsuceq0g  4403  abnex  4432  reg2exmidlema  4518  ordsuc  4547  onnmin  4552  ssnel  4553  ordtri2or2exmid  4555  ontri2orexmidim  4556  reg3exmidlemwe  4563  acexmidlemab  5847  reldmtpos  6232  dmtpos  6235  2pwuninelg  6262  onunsnss  6894  snon0  6913  nninfisol  7109  exmidomni  7118  pr2ne  7169  ltexprlemdisj  7568  recexprlemdisj  7592  caucvgprlemnkj  7628  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  inelr  8503  rimul  8504  recgt0  8766  zfz1iso  10776  isprm2  12071  nprmdvds1  12094  divgcdodd  12097  coprm  12098  coseq0q4123  13549  pwle2  14031  exmid1stab  14033  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048