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  1814  cbvexdh  1941  repizf2  4196  issref  5053  fnun  5367  ovigg  6047  tfrlem9  6386  tfri3  6434  ordge1n0im  6503  nntri3or  6560  updjud  7157  axprecex  7964  peano5nnnn  7976  peano5nni  9010  zeo  9448  nn0ind-raph  9460  fzm1  10192  fzind2  10332  fzfig  10539  bcpasc  10875  climrecvg1n  11530  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  bitsfzo  12137  gcdaddm  12176  coprmdvds1  12284  qredeq  12289  fiinopn  14324  zabsle1  15324  bj-intabssel  15519  triap  15760