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  5321  rexopabb  5434  tz6.12  6779  r1ord3  9471  brdom7disj  10218  brdom6disj  10219  alephadd  10264  ltresr  10827  divmuldiv  11605  fnn0ind  12349  rexanuz  14985  nprmi  16322  lsmvalx  19159  cncfval  23957  angval  25856  amgmlem  26044  sspval  28986  sshjval  29613  sshjval3  29617  hosmval  29998  hodmval  30000  hfsmval  30001  opreu2reuALT  30726  broutsideof3  34355  mptsnunlem  35436  relowlpssretop  35462  line2ylem  45985