Theorem mtoi 668

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 667	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 617  ax-in2 618

This theorem is referenced by:  mtbii  678  mtbiri  679  pwnss  4243  exmid1stab  4292  nsuceq0g  4509  abnex  4538  reg2exmidlema  4626  ordsuc  4655  onnmin  4660  ssnel  4661  ordtri2or2exmid  4663  ontri2orexmidim  4664  reg3exmidlemwe  4671  acexmidlemab  6001  reldmtpos  6405  dmtpos  6408  2pwuninelg  6435  onunsnss  7090  snon0  7113  nninfisol  7311  exmidomni  7320  pr2ne  7376  ltexprlemdisj  7804  recexprlemdisj  7828  caucvgprlemnkj  7864  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  inelr  8742  rimul  8743  recgt0  9008  zfz1iso  11076  isprm2  12655  nprmdvds1  12678  divgcdodd  12681  coprm  12682  coseq0q4123  15524  lgsquad2lem2  15777  umgrnloop0  15933  umgrislfupgrenlem  15944  lfgrnloopen  15947  3dom  16439  pwle2  16451  nninfalllem1  16462  nninfall  16463  nninfsellemqall  16469