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  5364  rexopabb  5501  tz6.12  6910  r1ord3  9793  brdom7disj  10614  brdom6disj  10615  alephadd  10666  ltresr  11229  divmuldiv  12021  fnn0ind  12802  rexanuz  15519  nprmi  16870  lsmvalx  19859  cncfval  25215  angval  27135  amgmlem  27323  sspval  31331  sshjval  31958  sshjval3  31962  hosmval  32343  hodmval  32345  hfsmval  32346  opreu2reuALT  33121  broutsideof3  36984  mptsnunlem  38355  relowlpssretop  38381  permac8prim  46098  line2ylem  49957