Theorem biimtrrdi 164

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
biimtrrdi.1	|- ( ph -> ( ch <-> ps ) )
biimtrrdi.2	|- ( ch -> th )

Assertion

Ref	Expression
biimtrrdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 |- ( ph -> ( ch <-> ps ) )
2	1	biimprd 158	. 2 |- ( ph -> ( ps -> ch ) )
3		biimtrrdi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistrfor  1846  cbvexdh  1973  repizf2  4246  issref  5111  fnun  5429  ovigg  6125  tfrlem9  6465  tfri3  6513  ordge1n0im  6582  nntri3or  6639  updjud  7249  axprecex  8067  peano5nnnn  8079  peano5nni  9113  zeo  9552  nn0ind-raph  9564  fzm1  10296  fzind2  10445  fzfig  10652  bcpasc  10988  climrecvg1n  11859  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  bitsfzo  12466  gcdaddm  12505  coprmdvds1  12613  qredeq  12618  fiinopn  14678  zabsle1  15678  incistruhgr  15890  wlk1walkdom  16070  bj-intabssel  16153  triap  16397