Theorem sylanbr 584

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syl2anbr  600  funfv  6749  2mpo0  7393  tfrlem7  8018  omword  8195  isinf  8730  fsuppunbi  8853  axdc3lem2  9872  supsrlem  10532  expclzlem  13452  expgt0  13461  expge0  13464  expge1  13465  swrdnd2  14016  resqrex  14609  rplpwr  15906  4sqlem19  16298  gexcl3  18711  thlle  20840  decpmataa0  21375  neindisj  21724  ptcmplem5  22663  tsmsxplem1  22760  tsmsxplem2  22761  elovolmr  24076  itgsubst  24645  logeftb  25166  logbchbase  25348  legov  26370  unopbd  29791  nmcoplb  29806  nmcfnlb  29830  nmopcoi  29871  iocinif  30503  voliune  31488  signstfvneq0  31842  lfuhgr3  32366  nosupbnd1lem5  33212  f1omptsnlem  34616  unccur  34874  matunitlindflem2  34888  stoweidlem15  42299  hoiqssbllem3  42905  vonioo  42963  vonicc  42966  gboge9  43928