Theorem sylanbr 580

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  syl2anbr  597  rspc4v  3629  funfv  6977  2mpo0  7657  tfrlem7  8385  omword  8572  isinf  9262  isinfOLD  9263  fsuppunbi  9386  axdc3lem2  10448  supsrlem  11108  expclzlem  14053  expgt0  14065  expge0  14068  expge1  14069  swrdnd2  14609  resqrex  15201  rplpwr  16503  4sqlem19  16900  gexcl3  19496  thlle  21470  thlleOLD  21471  decpmataa0  22490  neindisj  22841  ptcmplem5  23780  tsmsxplem1  23877  tsmsxplem2  23878  elovolmr  25225  itgsubst  25801  logeftb  26328  logbchbase  26512  nosupbnd1lem5  27451  noinfbnd1lem5  27466  legov  28103  unopbd  31535  nmcoplb  31550  nmcfnlb  31574  nmopcoi  31615  iocinif  32259  r1plmhm  32955  r1pquslmic  32956  voliune  33525  signstfvneq0  33881  lfuhgr3  34408  f1omptsnlem  36520  unccur  36774  matunitlindflem2  36788  stoweidlem15  45029  hoiqssbllem3  45638  vonioo  45696  vonicc  45699  gboge9  46730  catprs  47718