Theorem sylanbr 581

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 579	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  598  rspc4v  3655  funfv  7009  2mpo0  7699  tfrlem7  8439  omword  8626  isinf  9323  isinfOLD  9324  fsuppunbi  9458  axdc3lem2  10520  supsrlem  11180  expclzlem  14134  expgt0  14146  expge0  14149  expge1  14150  swrdnd2  14703  resqrex  15299  rplpwr  16605  4sqlem19  17010  gexcl3  19629  thlle  21739  thlleOLD  21740  decpmataa0  22795  neindisj  23146  ptcmplem5  24085  tsmsxplem1  24182  tsmsxplem2  24183  elovolmr  25530  itgsubst  26110  logeftb  26643  logbchbase  26832  nosupbnd1lem5  27775  noinfbnd1lem5  27790  legov  28611  unopbd  32047  nmcoplb  32062  nmcfnlb  32086  nmopcoi  32127  an52ds  32480  an62ds  32481  an72ds  32482  an82ds  32483  iocinif  32786  1arithufdlem4  33540  r1plmhm  33595  r1pquslmic  33596  voliune  34193  signstfvneq0  34549  lfuhgr3  35087  f1omptsnlem  37302  unccur  37563  matunitlindflem2  37577  stoweidlem15  45936  hoiqssbllem3  46545  vonioo  46603  vonicc  46606  gboge9  47638  catprs  48678