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  4250  issref  5117  fnun  5435  ovigg  6137  tfrlem9  6480  tfri3  6528  ordge1n0im  6599  nntri3or  6656  updjud  7272  axprecex  8090  peano5nnnn  8102  peano5nni  9136  zeo  9575  nn0ind-raph  9587  fzm1  10325  fzind2  10475  fzfig  10682  bcpasc  11018  climrecvg1n  11899  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  bitsfzo  12506  gcdaddm  12545  coprmdvds1  12653  qredeq  12658  fiinopn  14718  zabsle1  15718  incistruhgr  15931  wlk1walkdom  16156  isclwwlknx  16211  bj-intabssel  16321  triap  16569