Theorem syl2anbr 605

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  sylancbr  607  reusv2  5339  rexopabb  5477  tz6.12  6858  r1ord3  9704  brdom7disj  10451  brdom6disj  10452  alephadd  10498  ltresr  11061  divmuldiv  11853  fnn0ind  12626  rexanuz  15306  nprmi  16656  lsmvalx  19612  cncfval  24880  angval  26790  amgmlem  26978  sspval  30819  sshjval  31446  sshjval3  31450  hosmval  31831  hodmval  31833  hfsmval  31834  opreu2reuALT  32571  broutsideof3  36361  mptsnunlem  37707  relowlpssretop  37733  permac8prim  45465  line2ylem  49249