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  1823  cbvexdh  1950  repizf2  4207  issref  5066  fnun  5383  ovigg  6068  tfrlem9  6407  tfri3  6455  ordge1n0im  6524  nntri3or  6581  updjud  7186  axprecex  7995  peano5nnnn  8007  peano5nni  9041  zeo  9480  nn0ind-raph  9492  fzm1  10224  fzind2  10370  fzfig  10577  bcpasc  10913  climrecvg1n  11692  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  bitsfzo  12299  gcdaddm  12338  coprmdvds1  12446  qredeq  12451  fiinopn  14509  zabsle1  15509  bj-intabssel  15762  triap  16005