Theorem syl6bir 163

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
syl6bir.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
syl6bir.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6bir	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6bir

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 157	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bir.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistrfor  1777  cbvexdh  1903  repizf2  4118  issref  4961  fnun  5269  ovigg  5931  tfrlem9  6256  tfri3  6304  ordge1n0im  6373  nntri3or  6429  updjud  7012  axprecex  7779  peano5nnnn  7791  peano5nni  8815  zeo  9248  nn0ind-raph  9260  fzm1  9980  fzind2  10116  fzfig  10307  bcpasc  10617  climrecvg1n  11222  oddnn02np1  11744  oddge22np1  11745  evennn02n  11746  evennn2n  11747  gcdaddm  11840  coprmdvds1  11940  qredeq  11945  fiinopn  12349  bj-intabssel  13309  triap  13549