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  9779  brdom7disj  10528  brdom6disj  10529  alephadd  10574  ltresr  11137  divmuldiv  11916  fnn0ind  12663  rexanuz  15294  nprmi  16628  lsmvalx  19509  cncfval  24411  angval  26313  amgmlem  26501  sspval  30014  sshjval  30641  sshjval3  30645  hosmval  31026  hodmval  31028  hfsmval  31029  opreu2reuALT  31755  broutsideof3  35167  mptsnunlem  36305  relowlpssretop  36331  line2ylem  47515