Theorem sylanbr 585

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl2anbr  601  funfv  6725  2mpo0  7374  tfrlem7  8002  omword  8179  isinf  8715  fsuppunbi  8838  axdc3lem2  9862  supsrlem  10522  expclzlem  13449  expgt0  13458  expge0  13461  expge1  13462  swrdnd2  14008  resqrex  14602  rplpwr  15897  4sqlem19  16289  gexcl3  18704  thlle  20386  decpmataa0  21373  neindisj  21722  ptcmplem5  22661  tsmsxplem1  22758  tsmsxplem2  22759  elovolmr  24080  itgsubst  24652  logeftb  25175  logbchbase  25357  legov  26379  unopbd  29798  nmcoplb  29813  nmcfnlb  29837  nmopcoi  29878  iocinif  30530  voliune  31598  signstfvneq0  31952  lfuhgr3  32479  nosupbnd1lem5  33325  f1omptsnlem  34753  unccur  35040  matunitlindflem2  35054  stoweidlem15  42657  hoiqssbllem3  43263  vonioo  43321  vonicc  43324  gboge9  44282