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  5346  rexopabb  5484  tz6.12  6866  r1ord3  9708  brdom7disj  10455  brdom6disj  10456  alephadd  10502  ltresr  11065  divmuldiv  11857  fnn0ind  12630  rexanuz  15310  nprmi  16660  lsmvalx  19616  cncfval  24857  angval  26767  amgmlem  26955  sspval  30796  sshjval  31423  sshjval3  31427  hosmval  31808  hodmval  31810  hfsmval  31811  opreu2reuALT  32548  broutsideof3  36310  mptsnunlem  37656  relowlpssretop  37682  permac8prim  45443  line2ylem  49229