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 228	. 2 ⊢ (𝜑 → 𝜓)
3		sylanbr.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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  599  rspc4v  3621  funfv  6965  2mpo0  7654  tfrlem7  8395  omword  8580  isinf  9266  isinfOLD  9267  fsuppunbi  9399  axdc3lem2  10463  supsrlem  11123  expclzlem  14099  expgt0  14111  expge0  14114  expge1  14115  swrdnd2  14671  resqrex  15267  rplpwr  16575  4sqlem19  16981  gexcl3  19566  thlle  21655  decpmataa0  22704  neindisj  23053  ptcmplem5  23992  tsmsxplem1  24089  tsmsxplem2  24090  elovolmr  25427  itgsubst  26006  logeftb  26542  logbchbase  26731  nosupbnd1lem5  27674  noinfbnd1lem5  27689  legov  28510  unopbd  31942  nmcoplb  31957  nmcfnlb  31981  nmopcoi  32022  an52ds  32378  an62ds  32379  an72ds  32380  an82ds  32381  iocinif  32704  1arithufdlem4  33508  r1plmhm  33565  r1pquslmic  33566  voliune  34206  signstfvneq0  34550  lfuhgr3  35088  f1omptsnlem  37300  unccur  37573  matunitlindflem2  37587  stoweidlem15  45992  hoiqssbllem3  46601  vonioo  46659  vonicc  46662  gboge9  47726  catprs  48934