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 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  600  reusv2  5421  rexopabb  5547  tz6.12  6945  r1ord3  9851  brdom7disj  10600  brdom6disj  10601  alephadd  10646  ltresr  11209  divmuldiv  11994  fnn0ind  12742  rexanuz  15394  nprmi  16736  lsmvalx  19681  cncfval  24933  angval  26862  amgmlem  27051  sspval  30755  sshjval  31382  sshjval3  31386  hosmval  31767  hodmval  31769  hfsmval  31770  opreu2reuALT  32505  broutsideof3  36090  mptsnunlem  37304  relowlpssretop  37330  line2ylem  48485