Theorem syl2anbr 610

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anbr.1	⊢ (𝜓 ↔ 𝜑)
syl2anbr.2	⊢ (𝜒 ↔ 𝜏)
syl2anbr.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anbr	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2anbr

Step	Hyp	Ref	Expression
1		syl2anbr.2	. 2 ⊢ (𝜒 ↔ 𝜏)
2		syl2anbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
3		syl2anbr.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylanbr 593	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2br 606	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  sylancbr  612  reusv2  5372  rexopabb  5510  tz6.12  6903  r1ord3  9750  brdom7disj  10511  brdom6disj  10512  alephadd  10558  ltresr  11121  divmuldiv  11911  fnn0ind  12691  rexanuz  15393  nprmi  16743  lsmvalx  19705  cncfval  25012  angval  26928  amgmlem  27116  sspval  31012  sshjval  31639  sshjval3  31643  hosmval  32024  hodmval  32026  hfsmval  32027  opreu2reuALT  32760  broutsideof3  36513  mptsnunlem  37867  relowlpssretop  37893  permac8prim  45608  line2ylem  49409