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  5365  rexopabb  5502  tz6.12  6907  r1ord3  9782  brdom7disj  10603  brdom6disj  10604  alephadd  10655  ltresr  11218  divmuldiv  12010  fnn0ind  12791  rexanuz  15506  nprmi  16857  lsmvalx  19846  cncfval  25202  angval  27122  amgmlem  27310  sspval  31318  sshjval  31945  sshjval3  31949  hosmval  32330  hodmval  32332  hfsmval  32333  opreu2reuALT  33066  broutsideof3  36871  mptsnunlem  38241  relowlpssretop  38267  permac8prim  45982  line2ylem  49832