Theorem syl6bir 164

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 158	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bir.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistrfor  1800  cbvexdh  1926  repizf2  4162  issref  5011  fnun  5322  ovigg  5994  tfrlem9  6319  tfri3  6367  ordge1n0im  6436  nntri3or  6493  updjud  7080  axprecex  7878  peano5nnnn  7890  peano5nni  8921  zeo  9357  nn0ind-raph  9369  fzm1  10099  fzind2  10238  fzfig  10429  bcpasc  10745  climrecvg1n  11355  oddnn02np1  11884  oddge22np1  11885  evennn02n  11886  evennn2n  11887  gcdaddm  11984  coprmdvds1  12090  qredeq  12095  fiinopn  13474  zabsle1  14370  bj-intabssel  14511  triap  14747