Theorem mtoi 654

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 653	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 604  ax-in2 605

This theorem is referenced by:  mtbii  664  mtbiri  665  pwnss  4138  nsuceq0g  4396  abnex  4425  reg2exmidlema  4511  ordsuc  4540  onnmin  4545  ssnel  4546  ordtri2or2exmid  4548  ontri2orexmidim  4549  reg3exmidlemwe  4556  acexmidlemab  5836  reldmtpos  6221  dmtpos  6224  2pwuninelg  6251  onunsnss  6882  snon0  6901  nninfisol  7097  exmidomni  7106  pr2ne  7148  ltexprlemdisj  7547  recexprlemdisj  7571  caucvgprlemnkj  7607  caucvgprprlemnkltj  7630  caucvgprprlemnkeqj  7631  caucvgprprlemnjltk  7632  inelr  8482  rimul  8483  recgt0  8745  zfz1iso  10754  isprm2  12049  nprmdvds1  12072  divgcdodd  12075  coprm  12076  coseq0q4123  13395  pwle2  13878  exmid1stab  13880  nninfalllem1  13888  nninfall  13889  nninfsellemqall  13895