Theorem syl2anbr 600

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 583	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2br 596	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  602  reusv2  5350  rexopabb  5484  tz6.12  6866  r1ord3  9706  brdom7disj  10453  brdom6disj  10454  alephadd  10500  ltresr  11063  divmuldiv  11853  fnn0ind  12603  rexanuz  15281  nprmi  16628  lsmvalx  19580  cncfval  24849  angval  26779  amgmlem  26968  sspval  30810  sshjval  31437  sshjval3  31441  hosmval  31822  hodmval  31824  hfsmval  31825  opreu2reuALT  32562  broutsideof3  36339  mptsnunlem  37590  relowlpssretop  37616  permac8prim  45367  line2ylem  49108