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  1849  cbvexdh  1976  repizf2  4275  issref  5145  fnun  5464  ovigg  6174  tfrlem9  6550  tfri3  6598  ordge1n0im  6669  nntri3or  6726  updjud  7373  axprecex  8195  peano5nnnn  8207  peano5nni  9240  zeo  9683  nn0ind-raph  9695  fzm1  10434  fzind2  10585  fzfig  10792  bcpasc  11128  climrecvg1n  12033  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  bitsfzo  12641  gcdaddm  12680  coprmdvds1  12788  qredeq  12793  fiinopn  14869  zabsle1  15872  incistruhgr  16085  wlk1walkdom  16354  isclwwlknx  16411  bj-intabssel  16561  triap  16813