Theorem syl2anbr 592

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  sylancbr  594  reusv2  5105  tz6.12  6460  r1ord3  8929  brdom7disj  9675  brdom6disj  9676  alephadd  9721  ltresr  10284  divmuldiv  11058  fnn0ind  11811  rexanuz  14469  nprmi  15781  lsmvalx  18412  cncfval  23068  angval  24948  amgmlem  25136  sspval  28129  sshjval  28760  sshjval3  28764  hosmval  29145  hodmval  29147  hfsmval  29148  broutsideof3  32767  mptsnunlem  33730  relowlpssretop  33756  line2ylem  43317