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  4245  issref  5110  fnun  5428  ovigg  6124  tfrlem9  6463  tfri3  6511  ordge1n0im  6580  nntri3or  6637  updjud  7245  axprecex  8063  peano5nnnn  8075  peano5nni  9109  zeo  9548  nn0ind-raph  9560  fzm1  10292  fzind2  10440  fzfig  10647  bcpasc  10983  climrecvg1n  11854  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  bitsfzo  12461  gcdaddm  12500  coprmdvds1  12608  qredeq  12613  fiinopn  14672  zabsle1  15672  incistruhgr  15884  bj-intabssel  16111  triap  16356