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  6141  tfrlem9  6484  tfri3  6532  ordge1n0im  6603  nntri3or  6660  updjud  7280  axprecex  8099  peano5nnnn  8111  peano5nni  9145  zeo  9584  nn0ind-raph  9596  fzm1  10334  fzind2  10484  fzfig  10691  bcpasc  11027  climrecvg1n  11908  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  bitsfzo  12515  gcdaddm  12554  coprmdvds1  12662  qredeq  12667  fiinopn  14727  zabsle1  15727  incistruhgr  15940  wlk1walkdom  16209  isclwwlknx  16266  bj-intabssel  16385  triap  16633