Theorem biimtrrdi 164

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
biimtrrdi.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
biimtrrdi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
biimtrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 158	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  4196  issref  5053  fnun  5367  ovigg  6047  tfrlem9  6386  tfri3  6434  ordge1n0im  6503  nntri3or  6560  updjud  7157  axprecex  7966  peano5nnnn  7978  peano5nni  9012  zeo  9450  nn0ind-raph  9462  fzm1  10194  fzind2  10334  fzfig  10541  bcpasc  10877  climrecvg1n  11532  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  bitsfzo  12139  gcdaddm  12178  coprmdvds1  12286  qredeq  12291  fiinopn  14348  zabsle1  15348  bj-intabssel  15543  triap  15786