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  6131  tfrlem9  6471  tfri3  6519  ordge1n0im  6590  nntri3or  6647  updjud  7260  axprecex  8078  peano5nnnn  8090  peano5nni  9124  zeo  9563  nn0ind-raph  9575  fzm1  10308  fzind2  10457  fzfig  10664  bcpasc  11000  climrecvg1n  11875  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  bitsfzo  12482  gcdaddm  12521  coprmdvds1  12629  qredeq  12634  fiinopn  14694  zabsle1  15694  incistruhgr  15906  wlk1walkdom  16105  isclwwlknx  16158  bj-intabssel  16236  triap  16485