Theorem mtoi 674

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 673	1 |- ( ph -> -. ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mtbii  685  mtbiri  686  ifeqeqxdc  3687  pwnss  4296  exmid1stab  4345  nsuceq0g  4563  abnex  4593  reg2exmidlema  4681  ordsuc  4710  onnmin  4715  ssnel  4716  ordtri2or2exmid  4718  ontri2orexmidim  4719  reg3exmidlemwe  4726  acexmidlemab  6079  reldmtpos  6524  dmtpos  6527  2pwuninelg  6554  onunsnss  7224  snon0  7249  nninfisol  7473  exmidomni  7482  pr2ne  7538  ltexprlemdisj  7973  recexprlemdisj  7997  caucvgprlemnkj  8033  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  inelr  8912  rimul  8913  recgt0  9180  zfz1iso  11293  isprm2  12895  nprmdvds1  12918  divgcdodd  12921  coprm  12922  coseq0q4123  15935  lgsquad2lem2  16201  umgrnloop0  16358  umgrislfupgrenlem  16371  lfgrnloopen  16374  3dom  17018  pwle2  17028  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058