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  6594  tfri3  6642  ordge1n0im  6713  nntri3or  6770  updjud  7428  axprecex  8253  peano5nnnn  8265  peano5nni  9316  zeo  9762  nn0ind-raph  9774  fzm1  10524  fzind2  10675  fzfig  10888  bcpasc  11226  climrecvg1n  12139  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  bitsfzo  12747  gcdaddm  12786  coprmdvds1  12894  qredeq  12899  fiinopn  15230  bpos1lem  16309  zabsle1  16323  incistruhgr  16536  wlk1walkdom  16805  isclwwlknx  16862  bj-intabssel  17022  triap  17284