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  4252  issref  5119  fnun  5438  ovigg  6142  tfrlem9  6485  tfri3  6533  ordge1n0im  6604  nntri3or  6661  updjud  7281  axprecex  8100  peano5nnnn  8112  peano5nni  9146  zeo  9585  nn0ind-raph  9597  fzm1  10335  fzind2  10486  fzfig  10693  bcpasc  11029  climrecvg1n  11913  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  bitsfzo  12521  gcdaddm  12560  coprmdvds1  12668  qredeq  12673  fiinopn  14734  zabsle1  15734  incistruhgr  15947  wlk1walkdom  16216  isclwwlknx  16273  bj-intabssel  16411  triap  16659