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  3598  funfv  6931  2mpo0  7619  tfrlem7  8326  omword  8509  isinf  9179  fsuppunbi  9306  axdc3lem2  10375  supsrlem  11036  expclzlem  14020  expgt0  14032  expge0  14035  expge1  14036  swrdnd2  14593  resqrex  15187  rplpwr  16499  4sqlem19  16905  gexcl3  19533  thlle  21669  decpmataa0  22729  neindisj  23078  ptcmplem5  24017  tsmsxplem1  24114  tsmsxplem2  24115  elovolmr  25450  itgsubst  26029  logeftb  26565  logbchbase  26754  nosupbnd1lem5  27697  noinfbnd1lem5  27712  legov  28675  unopbd  32109  nmcoplb  32124  nmcfnlb  32148  nmopcoi  32189  an52ds  32544  an62ds  32545  an72ds  32546  an82ds  32547  iocinif  32878  1arithufdlem4  33646  r1plmhm  33709  r1pquslmic  33710  voliune  34413  signstfvneq0  34756  axprALT2  35293  lfuhgr3  35342  f1omptsnlem  37618  unccur  37883  matunitlindflem2  37897  stoweidlem15  46402  hoiqssbllem3  47011  vonioo  47069  vonicc  47072  gboge9  48153  catprs  49399