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  5995  reldmtpos  6399  dmtpos  6402  2pwuninelg  6429  onunsnss  7079  snon0  7102  nninfisol  7300  exmidomni  7309  pr2ne  7365  ltexprlemdisj  7793  recexprlemdisj  7817  caucvgprlemnkj  7853  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  caucvgprprlemnjltk  7878  inelr  8731  rimul  8732  recgt0  8997  zfz1iso  11063  isprm2  12639  nprmdvds1  12662  divgcdodd  12665  coprm  12666  coseq0q4123  15508  lgsquad2lem2  15761  umgrnloop0  15917  umgrislfupgrenlem  15928  lfgrnloopen  15931  pwle2  16364  nninfalllem1  16374  nninfall  16375  nninfsellemqall  16381