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  6529  dmtpos  6532  2pwuninelg  6559  onunsnss  7230  snon0  7255  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  11314  isprm2  12919  nprmdvds1  12943  divgcdodd  12946  coprm  12947  coseq0q4123  16078  lgsquad2lem2  16423  umgrnloop0  16580  umgrislfupgrenlem  16593  lfgrnloopen  16596  3dom  17240  pwle2  17250  idjudju  17269  nninfalllem1  17274  nninfall  17275  nninfsellemqall  17281