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 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  601  reusv2  5358  rexopabb  5488  tz6.12  6883  r1ord3  9735  brdom7disj  10484  brdom6disj  10485  alephadd  10530  ltresr  11093  divmuldiv  11882  fnn0ind  12633  rexanuz  15312  nprmi  16659  lsmvalx  19569  cncfval  24781  angval  26711  amgmlem  26900  sspval  30652  sshjval  31279  sshjval3  31283  hosmval  31664  hodmval  31666  hfsmval  31667  opreu2reuALT  32406  broutsideof3  36114  mptsnunlem  37326  relowlpssretop  37352  permac8prim  45004  line2ylem  48740