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  3592  funfv  6909  2mpo0  7595  tfrlem7  8302  omword  8485  isinf  9149  fsuppunbi  9273  axdc3lem2  10342  supsrlem  11002  expclzlem  13990  expgt0  14002  expge0  14005  expge1  14006  swrdnd2  14563  resqrex  15157  rplpwr  16469  4sqlem19  16875  gexcl3  19499  thlle  21634  decpmataa0  22683  neindisj  23032  ptcmplem5  23971  tsmsxplem1  24068  tsmsxplem2  24069  elovolmr  25404  itgsubst  25983  logeftb  26519  logbchbase  26708  nosupbnd1lem5  27651  noinfbnd1lem5  27666  legov  28563  unopbd  31995  nmcoplb  32010  nmcfnlb  32034  nmopcoi  32075  an52ds  32430  an62ds  32431  an72ds  32432  an82ds  32433  iocinif  32764  1arithufdlem4  33512  r1plmhm  33570  r1pquslmic  33571  voliune  34242  signstfvneq0  34585  lfuhgr3  35164  f1omptsnlem  37380  unccur  37642  matunitlindflem2  37656  stoweidlem15  46112  hoiqssbllem3  46721  vonioo  46779  vonicc  46782  gboge9  47863  catprs  49111