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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylancbr  602  reusv2  5295  rexopabb  5407  tz6.12  6687  r1ord3  9205  brdom7disj  9947  brdom6disj  9948  alephadd  9993  ltresr  10556  divmuldiv  11334  fnn0ind  12075  rexanuz  14699  nprmi  16027  lsmvalx  18758  cncfval  23490  angval  25373  amgmlem  25561  sspval  28494  sshjval  29121  sshjval3  29125  hosmval  29506  hodmval  29508  hfsmval  29509  opreu2reuALT  30234  broutsideof3  33582  mptsnunlem  34613  relowlpssretop  34639  line2ylem  44732