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  5376  rexopabb  5514  tz6.12  6909  r1ord3  9757  brdom7disj  10526  brdom6disj  10527  alephadd  10573  ltresr  11136  divmuldiv  11926  fnn0ind  12706  rexanuz  15416  nprmi  16764  lsmvalx  19732  cncfval  25076  angval  26995  amgmlem  27183  sspval  31104  sshjval  31731  sshjval3  31735  hosmval  32116  hodmval  32118  hfsmval  32119  opreu2reuALT  32852  broutsideof3  36631  mptsnunlem  38017  relowlpssretop  38043  permac8prim  45756  line2ylem  49564