Theorem sylanbr 582

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanbr.1	⊢ (𝜓 ↔ 𝜑)
sylanbr.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanbr	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanbr

Step	Hyp	Ref	Expression
1		sylanbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 227	. 2 ⊢ (𝜑 → 𝜓)
3		sylanbr.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  syl2anbr  599  rspc4v  3630  funfv  6978  2mpo0  7654  tfrlem7  8382  omword  8569  isinf  9259  isinfOLD  9260  fsuppunbi  9383  axdc3lem2  10445  supsrlem  11105  expclzlem  14048  expgt0  14060  expge0  14063  expge1  14064  swrdnd2  14604  resqrex  15196  rplpwr  16498  4sqlem19  16895  gexcl3  19454  thlle  21250  thlleOLD  21251  decpmataa0  22269  neindisj  22620  ptcmplem5  23559  tsmsxplem1  23656  tsmsxplem2  23657  elovolmr  24992  itgsubst  25565  logeftb  26091  logbchbase  26273  nosupbnd1lem5  27212  noinfbnd1lem5  27227  legov  27833  unopbd  31263  nmcoplb  31278  nmcfnlb  31302  nmopcoi  31343  iocinif  31987  voliune  33222  signstfvneq0  33578  lfuhgr3  34105  f1omptsnlem  36212  unccur  36466  matunitlindflem2  36480  stoweidlem15  44721  hoiqssbllem3  45330  vonioo  45388  vonicc  45391  gboge9  46422  catprs  47621