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  3595  funfv  6904  2mpo0  7590  tfrlem7  8297  omword  8480  isinf  9144  fsuppunbi  9268  axdc3lem2  10334  supsrlem  10994  expclzlem  13982  expgt0  13994  expge0  13997  expge1  13998  swrdnd2  14555  resqrex  15149  rplpwr  16461  4sqlem19  16867  gexcl3  19492  thlle  21627  decpmataa0  22676  neindisj  23025  ptcmplem5  23964  tsmsxplem1  24061  tsmsxplem2  24062  elovolmr  25397  itgsubst  25976  logeftb  26512  logbchbase  26701  nosupbnd1lem5  27644  noinfbnd1lem5  27659  legov  28556  unopbd  31985  nmcoplb  32000  nmcfnlb  32024  nmopcoi  32065  an52ds  32420  an62ds  32421  an72ds  32422  an82ds  32423  iocinif  32754  1arithufdlem4  33502  r1plmhm  33560  r1pquslmic  33561  voliune  34232  signstfvneq0  34575  lfuhgr3  35132  f1omptsnlem  37349  unccur  37622  matunitlindflem2  37636  stoweidlem15  46032  hoiqssbllem3  46641  vonioo  46699  vonicc  46702  gboge9  47774  catprs  49022