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  3608  funfv  6948  2mpo0  7638  tfrlem7  8351  omword  8534  isinf  9207  isinfOLD  9208  fsuppunbi  9340  axdc3lem2  10404  supsrlem  11064  expclzlem  14048  expgt0  14060  expge0  14063  expge1  14064  swrdnd2  14620  resqrex  15216  rplpwr  16528  4sqlem19  16934  gexcl3  19517  thlle  21606  decpmataa0  22655  neindisj  23004  ptcmplem5  23943  tsmsxplem1  24040  tsmsxplem2  24041  elovolmr  25377  itgsubst  25956  logeftb  26492  logbchbase  26681  nosupbnd1lem5  27624  noinfbnd1lem5  27639  legov  28512  unopbd  31944  nmcoplb  31959  nmcfnlb  31983  nmopcoi  32024  an52ds  32380  an62ds  32381  an72ds  32382  an82ds  32383  iocinif  32704  1arithufdlem4  33518  r1plmhm  33575  r1pquslmic  33576  voliune  34219  signstfvneq0  34563  lfuhgr3  35107  f1omptsnlem  37324  unccur  37597  matunitlindflem2  37611  stoweidlem15  46013  hoiqssbllem3  46622  vonioo  46680  vonicc  46683  gboge9  47765  catprs  49000