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  1848  cbvexdh  1975  repizf2  4258  issref  5126  fnun  5445  ovigg  6152  tfrlem9  6528  tfri3  6576  ordge1n0im  6647  nntri3or  6704  updjud  7324  axprecex  8143  peano5nnnn  8155  peano5nni  9188  zeo  9629  nn0ind-raph  9641  fzm1  10380  fzind2  10531  fzfig  10738  bcpasc  11074  climrecvg1n  11971  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  bitsfzo  12579  gcdaddm  12618  coprmdvds1  12726  qredeq  12731  fiinopn  14798  zabsle1  15801  incistruhgr  16014  wlk1walkdom  16283  isclwwlknx  16340  bj-intabssel  16490  triap  16744