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 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylancbr  601  reusv2  5341  rexopabb  5468  tz6.12  6846  r1ord3  9675  brdom7disj  10422  brdom6disj  10423  alephadd  10468  ltresr  11031  divmuldiv  11821  fnn0ind  12572  rexanuz  15253  nprmi  16600  lsmvalx  19552  cncfval  24809  angval  26739  amgmlem  26928  sspval  30701  sshjval  31328  sshjval3  31332  hosmval  31713  hodmval  31715  hfsmval  31716  opreu2reuALT  32454  broutsideof3  36166  mptsnunlem  37378  relowlpssretop  37404  permac8prim  45053  line2ylem  48789