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  1822  cbvexdh  1949  repizf2  4205  issref  5064  fnun  5381  ovigg  6065  tfrlem9  6404  tfri3  6452  ordge1n0im  6521  nntri3or  6578  updjud  7183  axprecex  7992  peano5nnnn  8004  peano5nni  9038  zeo  9477  nn0ind-raph  9489  fzm1  10221  fzind2  10366  fzfig  10573  bcpasc  10909  climrecvg1n  11601  oddnn02np1  12133  oddge22np1  12134  evennn02n  12135  evennn2n  12136  bitsfzo  12208  gcdaddm  12247  coprmdvds1  12355  qredeq  12360  fiinopn  14418  zabsle1  15418  bj-intabssel  15658  triap  15901