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  5372  rexopabb  5509  tz6.12  6940  r1ord3  9826  brdom7disj  10649  brdom6disj  10650  alephadd  10701  ltresr  11264  divmuldiv  12057  fnn0ind  12838  rexanuz  15557  nprmi  16908  lsmvalx  19904  cncfval  25264  angval  27186  amgmlem  27374  sspval  31382  sshjval  32009  sshjval3  32013  hosmval  32394  hodmval  32396  hfsmval  32397  opreu2reuALT  33172  broutsideof3  37106  mptsnunlem  38529  relowlpssretop  38555  permac8prim  46268  line2ylem  50194