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  5340  rexopabb  5476  tz6.12  6858  r1ord3  9697  brdom7disj  10444  brdom6disj  10445  alephadd  10491  ltresr  11054  divmuldiv  11846  fnn0ind  12619  rexanuz  15299  nprmi  16649  lsmvalx  19605  cncfval  24865  angval  26778  amgmlem  26967  sspval  30809  sshjval  31436  sshjval3  31440  hosmval  31821  hodmval  31823  hfsmval  31824  opreu2reuALT  32561  broutsideof3  36324  mptsnunlem  37668  relowlpssretop  37694  permac8prim  45459  line2ylem  49239