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  4160  issref  5008  fnun  5319  ovigg  5990  tfrlem9  6315  tfri3  6363  ordge1n0im  6432  nntri3or  6489  updjud  7076  axprecex  7874  peano5nnnn  7886  peano5nni  8916  zeo  9352  nn0ind-raph  9364  fzm1  10093  fzind2  10232  fzfig  10423  bcpasc  10737  climrecvg1n  11347  oddnn02np1  11875  oddge22np1  11876  evennn02n  11877  evennn2n  11878  gcdaddm  11975  coprmdvds1  12081  qredeq  12086  fiinopn  13284  zabsle1  14182  bj-intabssel  14312  triap  14548