Theorem syl2anbr 608

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylancbr  610  reusv2  5357  rexopabb  5495  tz6.12  6885  r1ord3  9733  brdom7disj  10481  brdom6disj  10482  alephadd  10528  ltresr  11091  divmuldiv  11884  fnn0ind  12665  rexanuz  15363  nprmi  16713  lsmvalx  19669  cncfval  24937  angval  26853  amgmlem  27041  sspval  30882  sshjval  31509  sshjval3  31513  hosmval  31894  hodmval  31896  hfsmval  31897  opreu2reuALT  32634  broutsideof3  36436  mptsnunlem  37792  relowlpssretop  37818  permac8prim  45550  line2ylem  49333