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  1814  cbvexdh  1941  repizf2  4195  issref  5052  fnun  5364  ovigg  6043  tfrlem9  6377  tfri3  6425  ordge1n0im  6494  nntri3or  6551  updjud  7148  axprecex  7947  peano5nnnn  7959  peano5nni  8993  zeo  9431  nn0ind-raph  9443  fzm1  10175  fzind2  10315  fzfig  10522  bcpasc  10858  climrecvg1n  11513  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  bitsfzo  12119  gcdaddm  12151  coprmdvds1  12259  qredeq  12264  fiinopn  14240  zabsle1  15240  bj-intabssel  15435  triap  15673