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  1811  cbvexdh  1938  repizf2  4192  issref  5049  fnun  5361  ovigg  6040  tfrlem9  6374  tfri3  6422  ordge1n0im  6491  nntri3or  6548  updjud  7143  axprecex  7942  peano5nnnn  7954  peano5nni  8987  zeo  9425  nn0ind-raph  9437  fzm1  10169  fzind2  10309  fzfig  10504  bcpasc  10840  climrecvg1n  11494  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  gcdaddm  12124  coprmdvds1  12232  qredeq  12237  fiinopn  14183  zabsle1  15156  bj-intabssel  15351  triap  15589