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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  exdistrfor  1853  cbvexdh  1982  repizf2  4301  issref  5173  fnun  5492  ovigg  6212  tfrlem9  6595  tfri3  6643  ordge1n0im  6714  nntri3or  6771  updjud  7428  axprecex  8253  peano5nnnn  8265  peano5nni  9316  zeo  9761  nn0ind-raph  9773  fzm1  10523  fzind2  10674  fzfig  10887  bcpasc  11225  climrecvg1n  12138  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  bitsfzo  12746  gcdaddm  12785  coprmdvds1  12893  qredeq  12898  fiinopn  15247  bpos1lem  16326  zabsle1  16340  incistruhgr  16553  wlk1walkdom  16822  isclwwlknx  16879  bj-intabssel  17039  triap  17301