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  1848  cbvexdh  1975  repizf2  4252  issref  5119  fnun  5438  ovigg  6142  tfrlem9  6485  tfri3  6533  ordge1n0im  6604  nntri3or  6661  updjud  7281  axprecex  8100  peano5nnnn  8112  peano5nni  9146  zeo  9585  nn0ind-raph  9597  fzm1  10335  fzind2  10486  fzfig  10693  bcpasc  11029  climrecvg1n  11926  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  bitsfzo  12534  gcdaddm  12573  coprmdvds1  12681  qredeq  12686  fiinopn  14747  zabsle1  15747  incistruhgr  15960  wlk1walkdom  16229  isclwwlknx  16286  bj-intabssel  16436  triap  16684