Theorem syl2anbr 600

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 583	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2br 596	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  602  reusv2  5345  rexopabb  5483  tz6.12  6864  r1ord3  9706  brdom7disj  10453  brdom6disj  10454  alephadd  10500  ltresr  11063  divmuldiv  11855  fnn0ind  12628  rexanuz  15308  nprmi  16658  lsmvalx  19614  cncfval  24855  angval  26765  amgmlem  26953  sspval  30794  sshjval  31421  sshjval3  31425  hosmval  31806  hodmval  31808  hfsmval  31809  opreu2reuALT  32546  broutsideof3  36308  mptsnunlem  37654  relowlpssretop  37680  permac8prim  45441  line2ylem  49227