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  3642  funfv  6996  2mpo0  7682  tfrlem7  8423  omword  8608  isinf  9296  isinfOLD  9297  fsuppunbi  9429  axdc3lem2  10491  supsrlem  11151  expclzlem  14124  expgt0  14136  expge0  14139  expge1  14140  swrdnd2  14693  resqrex  15289  rplpwr  16595  4sqlem19  17001  gexcl3  19605  thlle  21716  thlleOLD  21717  decpmataa0  22774  neindisj  23125  ptcmplem5  24064  tsmsxplem1  24161  tsmsxplem2  24162  elovolmr  25511  itgsubst  26090  logeftb  26625  logbchbase  26814  nosupbnd1lem5  27757  noinfbnd1lem5  27772  legov  28593  unopbd  32034  nmcoplb  32049  nmcfnlb  32073  nmopcoi  32114  an52ds  32470  an62ds  32471  an72ds  32472  an82ds  32473  iocinif  32783  1arithufdlem4  33575  r1plmhm  33630  r1pquslmic  33631  voliune  34230  signstfvneq0  34587  lfuhgr3  35125  f1omptsnlem  37337  unccur  37610  matunitlindflem2  37624  stoweidlem15  46030  hoiqssbllem3  46639  vonioo  46697  vonicc  46700  gboge9  47751  catprs  48900