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  1853  cbvexdh  1982  repizf2  4294  issref  5165  fnun  5484  ovigg  6199  tfrlem9  6580  tfri3  6628  ordge1n0im  6699  nntri3or  6756  updjud  7412  axprecex  8237  peano5nnnn  8249  peano5nni  9286  zeo  9730  nn0ind-raph  9742  fzm1  10485  fzind2  10636  fzfig  10845  bcpasc  11182  climrecvg1n  12092  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  bitsfzo  12700  gcdaddm  12739  coprmdvds1  12847  qredeq  12852  fiinopn  15028  zabsle1  16032  incistruhgr  16245  wlk1walkdom  16514  isclwwlknx  16571  bj-intabssel  16731  triap  16983