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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylancbr  602  reusv2  5303  rexopabb  5414  tz6.12  6692  r1ord3  9210  brdom7disj  9952  brdom6disj  9953  alephadd  9998  ltresr  10561  divmuldiv  11339  fnn0ind  12080  rexanuz  14704  nprmi  16032  lsmvalx  18763  cncfval  23495  angval  25378  amgmlem  25566  sspval  28499  sshjval  29126  sshjval3  29130  hosmval  29511  hodmval  29513  hfsmval  29514  opreu2reuALT  30239  broutsideof3  33587  mptsnunlem  34618  relowlpssretop  34644  line2ylem  44737