Theorem syl2anbr 601

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylancbr  603  reusv2  5269  rexopabb  5380  tz6.12  6668  r1ord3  9195  brdom7disj  9942  brdom6disj  9943  alephadd  9988  ltresr  10551  divmuldiv  11329  fnn0ind  12069  rexanuz  14697  nprmi  16023  lsmvalx  18756  cncfval  23493  angval  25387  amgmlem  25575  sspval  28506  sshjval  29133  sshjval3  29137  hosmval  29518  hodmval  29520  hfsmval  29521  opreu2reuALT  30247  broutsideof3  33700  mptsnunlem  34755  relowlpssretop  34781  line2ylem  45165