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  4258  issref  5126  fnun  5445  ovigg  6152  tfrlem9  6528  tfri3  6576  ordge1n0im  6647  nntri3or  6704  updjud  7341  axprecex  8160  peano5nnnn  8172  peano5nni  9205  zeo  9646  nn0ind-raph  9658  fzm1  10397  fzind2  10548  fzfig  10755  bcpasc  11091  climrecvg1n  11988  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  bitsfzo  12596  gcdaddm  12635  coprmdvds1  12743  qredeq  12748  fiinopn  14815  zabsle1  15818  incistruhgr  16031  wlk1walkdom  16300  isclwwlknx  16357  bj-intabssel  16507  triap  16761