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  3611  funfv  6951  2mpo0  7641  tfrlem7  8354  omword  8537  isinf  9214  isinfOLD  9215  fsuppunbi  9347  axdc3lem2  10411  supsrlem  11071  expclzlem  14055  expgt0  14067  expge0  14070  expge1  14071  swrdnd2  14627  resqrex  15223  rplpwr  16535  4sqlem19  16941  gexcl3  19524  thlle  21613  decpmataa0  22662  neindisj  23011  ptcmplem5  23950  tsmsxplem1  24047  tsmsxplem2  24048  elovolmr  25384  itgsubst  25963  logeftb  26499  logbchbase  26688  nosupbnd1lem5  27631  noinfbnd1lem5  27646  legov  28519  unopbd  31951  nmcoplb  31966  nmcfnlb  31990  nmopcoi  32031  an52ds  32387  an62ds  32388  an72ds  32389  an82ds  32390  iocinif  32711  1arithufdlem4  33525  r1plmhm  33582  r1pquslmic  33583  voliune  34226  signstfvneq0  34570  lfuhgr3  35114  f1omptsnlem  37331  unccur  37604  matunitlindflem2  37618  stoweidlem15  46020  hoiqssbllem3  46629  vonioo  46687  vonicc  46690  gboge9  47769  catprs  49004