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  5391  rexopabb  5518  tz6.12  6906  r1ord3  9772  brdom7disj  10521  brdom6disj  10522  alephadd  10567  ltresr  11130  divmuldiv  11910  fnn0ind  12657  rexanuz  15288  nprmi  16622  lsmvalx  19544  cncfval  24718  angval  26637  amgmlem  26826  sspval  30400  sshjval  31027  sshjval3  31031  hosmval  31412  hodmval  31414  hfsmval  31415  opreu2reuALT  32141  broutsideof3  35559  mptsnunlem  36675  relowlpssretop  36701  line2ylem  47591