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  1846  cbvexdh  1973  repizf2  4246  issref  5111  fnun  5429  ovigg  6131  tfrlem9  6471  tfri3  6519  ordge1n0im  6590  nntri3or  6647  updjud  7260  axprecex  8078  peano5nnnn  8090  peano5nni  9124  zeo  9563  nn0ind-raph  9575  fzm1  10308  fzind2  10457  fzfig  10664  bcpasc  11000  climrecvg1n  11874  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  bitsfzo  12481  gcdaddm  12520  coprmdvds1  12628  qredeq  12633  fiinopn  14693  zabsle1  15693  incistruhgr  15905  wlk1walkdom  16100  bj-intabssel  16208  triap  16457