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  5402  rexopabb  5532  tz6.12  6930  r1ord3  9823  brdom7disj  10572  brdom6disj  10573  alephadd  10618  ltresr  11181  divmuldiv  11968  fnn0ind  12719  rexanuz  15385  nprmi  16727  lsmvalx  19658  cncfval  24915  angval  26845  amgmlem  27034  sspval  30743  sshjval  31370  sshjval3  31374  hosmval  31755  hodmval  31757  hfsmval  31758  opreu2reuALT  32497  broutsideof3  36128  mptsnunlem  37340  relowlpssretop  37366  line2ylem  48677