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  4191  issref  5048  fnun  5360  ovigg  6039  tfrlem9  6372  tfri3  6420  ordge1n0im  6489  nntri3or  6546  updjud  7141  axprecex  7940  peano5nnnn  7952  peano5nni  8985  zeo  9422  nn0ind-raph  9434  fzm1  10166  fzind2  10306  fzfig  10501  bcpasc  10837  climrecvg1n  11491  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  gcdaddm  12121  coprmdvds1  12229  qredeq  12234  fiinopn  14172  zabsle1  15115  bj-intabssel  15281  triap  15519