Theorem syl2anbr 610

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylancbr  612  reusv2  5376  rexopabb  5514  tz6.12  6907  r1ord3  9755  brdom7disj  10516  brdom6disj  10517  alephadd  10563  ltresr  11126  divmuldiv  11916  fnn0ind  12696  rexanuz  15399  nprmi  16748  lsmvalx  19710  cncfval  25028  angval  26947  amgmlem  27135  sspval  31056  sshjval  31683  sshjval3  31687  hosmval  32068  hodmval  32070  hfsmval  32071  opreu2reuALT  32804  broutsideof3  36599  mptsnunlem  37965  relowlpssretop  37991  permac8prim  45706  line2ylem  49514