Theorem syl2anbr 598

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  sylancbr  600  reusv2  5402  rexopabb  5529  tz6.12  6917  r1ord3  9780  brdom7disj  10529  brdom6disj  10530  alephadd  10575  ltresr  11138  divmuldiv  11919  fnn0ind  12666  rexanuz  15297  nprmi  16631  lsmvalx  19549  cncfval  24629  angval  26539  amgmlem  26727  sspval  30240  sshjval  30867  sshjval3  30871  hosmval  31252  hodmval  31254  hfsmval  31255  opreu2reuALT  31981  broutsideof3  35399  mptsnunlem  36523  relowlpssretop  36549  line2ylem  47526