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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistrfor  1752  cbvexdh  1874  repizf2  4044  issref  4877  fnun  5185  ovigg  5843  tfrlem9  6168  tfri3  6216  ordge1n0im  6285  nntri3or  6341  updjud  6917  axprecex  7609  peano5nnnn  7621  peano5nni  8627  zeo  9054  nn0ind-raph  9066  fzm1  9767  fzind2  9903  fzfig  10090  bcpasc  10399  climrecvg1n  11003  oddnn02np1  11419  oddge22np1  11420  evennn02n  11421  evennn2n  11422  gcdaddm  11514  coprmdvds1  11612  qredeq  11617  fiinopn  12008  bj-intabssel  12679  triap  12905