Theorem mtoi 622

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 621	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 576  ax-in2 577

This theorem is referenced by:  mtbii  631  mtbiri  632  pwnss  3933  nsuceq0g  4173  reg2exmidlema  4277  ordsuc  4306  onnmin  4311  ssnel  4312  ordtri2or2exmid  4314  reg3exmidlemwe  4321  acexmidlemab  5526  reldmtpos  5891  dmtpos  5894  2pwuninelg  5921  onunsnss  6383  snon0  6387  pr2ne  6461  ltexprlemdisj  6796  recexprlemdisj  6820  caucvgprlemnkj  6856  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  inelr  7684  rimul  7685  recgt0  7928  isprm2  10499  nprmdvds1  10521  divgcdodd  10522  coprm  10523