Theorem syl2anbr 611

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylancbr  613  reusv2  5368  rexopabb  5506  tz6.12  6902  r1ord3  9764  brdom7disj  10534  brdom6disj  10535  alephadd  10586  ltresr  11149  divmuldiv  11939  fnn0ind  12720  rexanuz  15433  nprmi  16779  lsmvalx  19766  cncfval  25116  angval  27038  amgmlem  27226  sspval  31204  sshjval  31831  sshjval3  31835  hosmval  32216  hodmval  32218  hfsmval  32219  opreu2reuALT  32952  broutsideof3  36706  mptsnunlem  38092  relowlpssretop  38118  permac8prim  45837  line2ylem  49681