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  4298  exmid1stab  4347  nsuceq0g  4565  abnex  4595  reg2exmidlema  4683  ordsuc  4712  onnmin  4717  ssnel  4718  ordtri2or2exmid  4720  ontri2orexmidim  4721  reg3exmidlemwe  4728  acexmidlemab  6082  reldmtpos  6528  dmtpos  6531  2pwuninelg  6558  onunsnss  7228  snon0  7253  nninfisol  7479  exmidomni  7488  pr2ne  7544  ltexprlemdisj  7979  recexprlemdisj  8003  caucvgprlemnkj  8039  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  inelr  8920  rimul  8921  recgt0  9188  zfz1iso  11315  isprm2  12920  nprmdvds1  12944  divgcdodd  12947  coprm  12948  coseq0q4123  16061  lgsquad2lem2  16406  umgrnloop0  16563  umgrislfupgrenlem  16576  lfgrnloopen  16579  3dom  17223  pwle2  17233  idjudju  17252  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264