Theorem sylanbr 583

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 228	. 2 ⊢ (𝜑 → 𝜓)
3		sylanbr.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 581	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syl2anbr  600  rspc4v  3597  funfv  6922  2mpo0  7609  tfrlem7  8316  omword  8499  isinf  9169  fsuppunbi  9296  axdc3lem2  10365  supsrlem  11026  expclzlem  14010  expgt0  14022  expge0  14025  expge1  14026  swrdnd2  14583  resqrex  15177  rplpwr  16489  4sqlem19  16895  gexcl3  19520  thlle  21656  decpmataa0  22716  neindisj  23065  ptcmplem5  24004  tsmsxplem1  24101  tsmsxplem2  24102  elovolmr  25437  itgsubst  26016  logeftb  26552  logbchbase  26741  nosupbnd1lem5  27684  noinfbnd1lem5  27699  legov  28661  unopbd  32094  nmcoplb  32109  nmcfnlb  32133  nmopcoi  32174  an52ds  32529  an62ds  32530  an72ds  32531  an82ds  32532  iocinif  32863  1arithufdlem4  33630  r1plmhm  33693  r1pquslmic  33694  voliune  34388  signstfvneq0  34731  lfuhgr3  35316  f1omptsnlem  37543  unccur  37806  matunitlindflem2  37820  stoweidlem15  46326  hoiqssbllem3  46935  vonioo  46993  vonicc  46996  gboge9  48077  catprs  49323