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  4299  issref  5170  fnun  5489  ovigg  6209  tfrlem9  6590  tfri3  6638  ordge1n0im  6709  nntri3or  6766  updjud  7423  axprecex  8248  peano5nnnn  8260  peano5nni  9310  zeo  9756  nn0ind-raph  9768  fzm1  10518  fzind2  10669  fzfig  10882  bcpasc  11220  climrecvg1n  12133  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  bitsfzo  12741  gcdaddm  12780  coprmdvds1  12888  qredeq  12893  fiinopn  15196  bpos1lem  16270  zabsle1  16284  incistruhgr  16497  wlk1walkdom  16766  isclwwlknx  16823  bj-intabssel  16983  triap  17244