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  8914  rimul  8915  recgt0  9182  zfz1iso  11307  isprm2  12911  nprmdvds1  12935  divgcdodd  12938  coprm  12939  coseq0q4123  15985  lgsquad2lem2  16299  umgrnloop0  16456  umgrislfupgrenlem  16469  lfgrnloopen  16472  3dom  17116  pwle2  17126  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156