Theorem sylanbr 571

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  syl2anbr  586  funfv  6407  2mpt20  7029  tfrlem7  7632  omword  7804  isinf  8329  fsuppunbi  8452  axdc3lem2  9475  supsrlem  10134  expclzlem  13091  expgt0  13100  expge0  13103  expge1  13104  swrdnd2  13642  resqrex  14199  rplpwr  15484  4sqlem19  15874  gexcl3  18209  thlle  20258  decpmataa0  20793  neindisj  21142  ptcmplem5  22080  tsmsxplem1  22176  tsmsxplem2  22177  elovolmr  23464  itgsubst  24032  logeftb  24551  logbchbase  24730  legov  25701  unopbd  29214  nmcoplb  29229  nmcfnlb  29253  nmopcoi  29294  iocinif  29883  voliune  30632  signstfvneq0  30989  nosupbnd1lem5  32195  f1omptsnlem  33520  unccur  33725  matunitlindflem2  33739  stoweidlem15  40749  hoiqssbllem3  41358  vonioo  41416  vonicc  41419  gboge9  42180