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  7474  exmidomni  7483  pr2ne  7539  ltexprlemdisj  7974  recexprlemdisj  7998  caucvgprlemnkj  8034  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnjltk  8059  inelr  8915  rimul  8916  recgt0  9183  zfz1iso  11309  isprm2  12914  nprmdvds1  12938  divgcdodd  12941  coprm  12942  coseq0q4123  16027  lgsquad2lem2  16367  umgrnloop0  16524  umgrislfupgrenlem  16537  lfgrnloopen  16540  3dom  17184  pwle2  17194  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224