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  3594  funfv  6919  2mpo0  7605  tfrlem7  8312  omword  8495  isinf  9163  fsuppunbi  9290  axdc3lem2  10359  supsrlem  11020  expclzlem  14004  expgt0  14016  expge0  14019  expge1  14020  swrdnd2  14577  resqrex  15171  rplpwr  16483  4sqlem19  16889  gexcl3  19514  thlle  21650  decpmataa0  22710  neindisj  23059  ptcmplem5  23998  tsmsxplem1  24095  tsmsxplem2  24096  elovolmr  25431  itgsubst  26010  logeftb  26546  logbchbase  26735  nosupbnd1lem5  27678  noinfbnd1lem5  27693  legov  28606  unopbd  32039  nmcoplb  32054  nmcfnlb  32078  nmopcoi  32119  an52ds  32474  an62ds  32475  an72ds  32476  an82ds  32477  iocinif  32810  1arithufdlem4  33577  r1plmhm  33640  r1pquslmic  33641  voliune  34335  signstfvneq0  34678  lfuhgr3  35263  f1omptsnlem  37480  unccur  37743  matunitlindflem2  37757  stoweidlem15  46201  hoiqssbllem3  46810  vonioo  46868  vonicc  46871  gboge9  47952  catprs  49198