Theorem sylanbr 591

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  syl2anbr  608  rspc4v  3603  funfv  6956  2mpo0  7647  tfrlem7  8356  omword  8541  isinf  9211  fsuppunbi  9337  axdc3lem2  10410  supsrlem  11071  expclzlem  14098  expgt0  14110  expge0  14113  expge1  14114  swrdnd2  14671  resqrex  15279  rplpwr  16594  4sqlem19  17001  gexcl3  19629  thlle  21751  decpmataa0  22830  neindisj  23179  ptcmplem5  24118  tsmsxplem1  24215  tsmsxplem2  24216  elovolmr  25540  itgsubst  26113  logeftb  26650  logbchbase  26838  nosupbnd1lem5  27778  noinfbnd1lem5  27793  legov  28756  unopbd  32220  nmcoplb  32235  nmcfnlb  32259  nmopcoi  32300  an52ds  32655  an62ds  32656  an72ds  32657  an82ds  32658  iocinif  32985  1arithufdlem4  33745  r1plmhm  33808  r1pquslmic  33809  voliune  34528  signstfvneq0  34868  axprALT2  35409  lfuhgr3  35475  f1omptsnlem  37835  unccur  38107  matunitlindflem2  38121  stoweidlem15  46594  hoiqssbllem3  47203  vonioo  47261  vonicc  47264  gboge9  48391  catprs  49637