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  1824  cbvexdh  1951  repizf2  4222  issref  5084  fnun  5401  ovigg  6089  tfrlem9  6428  tfri3  6476  ordge1n0im  6545  nntri3or  6602  updjud  7210  axprecex  8028  peano5nnnn  8040  peano5nni  9074  zeo  9513  nn0ind-raph  9525  fzm1  10257  fzind2  10405  fzfig  10612  bcpasc  10948  climrecvg1n  11774  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  bitsfzo  12381  gcdaddm  12420  coprmdvds1  12528  qredeq  12533  fiinopn  14591  zabsle1  15591  incistruhgr  15801  bj-intabssel  15925  triap  16170