Theorem sylanbr 490

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 488	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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 386

This theorem is referenced by:  syl2anbr  497  funfv  6252  2mpt20  6867  tfrlem7  7464  omword  7635  isinf  8158  fsuppunbi  8281  axdc3lem2  9258  supsrlem  9917  expclzlem  12867  expgt0  12876  expge0  12879  expge1  12880  swrdnd2  13415  resqrex  13972  rplpwr  15257  isprm2lem  15375  4sqlem19  15648  gexcl3  17983  thlle  20022  decpmataa0  20554  neindisj  20902  ptcmplem5  21841  tsmsxplem1  21937  tsmsxplem2  21938  elovolmr  23225  itgsubst  23793  logeftb  24311  logbchbase  24490  legov  25461  unopbd  28844  nmcoplb  28859  nmcfnlb  28883  nmopcoi  28924  iocinif  29517  voliune  30266  signstfvneq0  30623  nosupbnd1lem5  31832  f1omptsnlem  33154  unccur  33363  matunitlindflem2  33377  stoweidlem15  39995  hoiqssbllem3  40601  vonioo  40659  vonicc  40662  gboge9  41417