Theorem mtoi 666

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 615  ax-in2 616

This theorem is referenced by:  mtbii  676  mtbiri  677  pwnss  4219  exmid1stab  4268  nsuceq0g  4483  abnex  4512  reg2exmidlema  4600  ordsuc  4629  onnmin  4634  ssnel  4635  ordtri2or2exmid  4637  ontri2orexmidim  4638  reg3exmidlemwe  4645  acexmidlemab  5961  reldmtpos  6362  dmtpos  6365  2pwuninelg  6392  onunsnss  7040  snon0  7063  nninfisol  7261  exmidomni  7270  pr2ne  7326  ltexprlemdisj  7754  recexprlemdisj  7778  caucvgprlemnkj  7814  caucvgprprlemnkltj  7837  caucvgprprlemnkeqj  7838  caucvgprprlemnjltk  7839  inelr  8692  rimul  8693  recgt0  8958  zfz1iso  11023  isprm2  12554  nprmdvds1  12577  divgcdodd  12580  coprm  12581  coseq0q4123  15421  lgsquad2lem2  15674  umgrislfupgrenlem  15836  lfgrnloopen  15839  pwle2  16137  nninfalllem1  16147  nninfall  16148  nninfsellemqall  16154