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  3641  funfv  6995  2mpo0  7681  tfrlem7  8421  omword  8606  isinf  9293  isinfOLD  9294  fsuppunbi  9426  axdc3lem2  10488  supsrlem  11148  expclzlem  14120  expgt0  14132  expge0  14135  expge1  14136  swrdnd2  14689  resqrex  15285  rplpwr  16591  4sqlem19  16996  gexcl3  19619  thlle  21733  thlleOLD  21734  decpmataa0  22789  neindisj  23140  ptcmplem5  24079  tsmsxplem1  24176  tsmsxplem2  24177  elovolmr  25524  itgsubst  26104  logeftb  26639  logbchbase  26828  nosupbnd1lem5  27771  noinfbnd1lem5  27786  legov  28607  unopbd  32043  nmcoplb  32058  nmcfnlb  32082  nmopcoi  32123  an52ds  32479  an62ds  32480  an72ds  32481  an82ds  32482  iocinif  32789  1arithufdlem4  33554  r1plmhm  33609  r1pquslmic  33610  voliune  34209  signstfvneq0  34565  lfuhgr3  35103  f1omptsnlem  37318  unccur  37589  matunitlindflem2  37603  stoweidlem15  45970  hoiqssbllem3  46579  vonioo  46637  vonicc  46640  gboge9  47688  catprs  48799