Theorem syl2anbr 599

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 582	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2br 595	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  601  reusv2  5361  rexopabb  5491  tz6.12  6886  r1ord3  9742  brdom7disj  10491  brdom6disj  10492  alephadd  10537  ltresr  11100  divmuldiv  11889  fnn0ind  12640  rexanuz  15319  nprmi  16666  lsmvalx  19576  cncfval  24788  angval  26718  amgmlem  26907  sspval  30659  sshjval  31286  sshjval3  31290  hosmval  31671  hodmval  31673  hfsmval  31674  opreu2reuALT  32413  broutsideof3  36121  mptsnunlem  37333  relowlpssretop  37359  permac8prim  45011  line2ylem  48744