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  1772  cbvexdh  1898  repizf2  4086  issref  4921  fnun  5229  ovigg  5891  tfrlem9  6216  tfri3  6264  ordge1n0im  6333  nntri3or  6389  updjud  6967  axprecex  7688  peano5nnnn  7700  peano5nni  8723  zeo  9156  nn0ind-raph  9168  fzm1  9880  fzind2  10016  fzfig  10203  bcpasc  10512  climrecvg1n  11117  oddnn02np1  11577  oddge22np1  11578  evennn02n  11579  evennn2n  11580  gcdaddm  11672  coprmdvds1  11772  qredeq  11777  fiinopn  12171  bj-intabssel  12996  triap  13224