Theorem syl2anbr 599

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 582	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2br 595	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sylancbr  601  reusv2  5326  rexopabb  5441  tz6.12  6797  r1ord3  9540  brdom7disj  10287  brdom6disj  10288  alephadd  10333  ltresr  10896  divmuldiv  11675  fnn0ind  12419  rexanuz  15057  nprmi  16394  lsmvalx  19244  cncfval  24051  angval  25951  amgmlem  26139  sspval  29085  sshjval  29712  sshjval3  29716  hosmval  30097  hodmval  30099  hfsmval  30100  opreu2reuALT  30825  broutsideof3  34428  mptsnunlem  35509  relowlpssretop  35535  line2ylem  46097