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  1823  cbvexdh  1950  repizf2  4206  issref  5065  fnun  5382  ovigg  6066  tfrlem9  6405  tfri3  6453  ordge1n0im  6522  nntri3or  6579  updjud  7184  axprecex  7993  peano5nnnn  8005  peano5nni  9039  zeo  9478  nn0ind-raph  9490  fzm1  10222  fzind2  10368  fzfig  10575  bcpasc  10911  climrecvg1n  11659  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  bitsfzo  12266  gcdaddm  12305  coprmdvds1  12413  qredeq  12418  fiinopn  14476  zabsle1  15476  bj-intabssel  15725  triap  15968