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  1978  repizf2  4280  issref  5150  fnun  5469  ovigg  6182  tfrlem9  6563  tfri3  6611  ordge1n0im  6682  nntri3or  6739  updjud  7386  axprecex  8211  peano5nnnn  8223  peano5nni  9257  zeo  9701  nn0ind-raph  9713  fzm1  10456  fzind2  10607  fzfig  10816  bcpasc  11153  climrecvg1n  12058  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  bitsfzo  12666  gcdaddm  12705  coprmdvds1  12813  qredeq  12818  fiinopn  14995  zabsle1  15998  incistruhgr  16211  wlk1walkdom  16480  isclwwlknx  16537  bj-intabssel  16687  triap  16939