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 205   ∧ 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 206  df-an 397

This theorem is referenced by:  sylancbr  601  reusv2  5401  rexopabb  5528  tz6.12  6916  r1ord3  9776  brdom7disj  10525  brdom6disj  10526  alephadd  10571  ltresr  11134  divmuldiv  11913  fnn0ind  12660  rexanuz  15291  nprmi  16625  lsmvalx  19506  cncfval  24403  angval  26303  amgmlem  26491  sspval  29971  sshjval  30598  sshjval3  30602  hosmval  30983  hodmval  30985  hfsmval  30986  opreu2reuALT  31712  broutsideof3  35093  mptsnunlem  36214  relowlpssretop  36240  line2ylem  47427