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  6752  2mpo0  7396  tfrlem7  8021  omword  8198  isinf  8733  fsuppunbi  8856  axdc3lem2  9875  supsrlem  10535  expclzlem  13456  expgt0  13465  expge0  13468  expge1  13469  swrdnd2  14019  resqrex  14612  rplpwr  15909  4sqlem19  16301  gexcl3  18714  thlle  20843  decpmataa0  21378  neindisj  21727  ptcmplem5  22666  tsmsxplem1  22763  tsmsxplem2  22764  elovolmr  24079  itgsubst  24648  logeftb  25169  logbchbase  25351  legov  26373  unopbd  29794  nmcoplb  29809  nmcfnlb  29833  nmopcoi  29874  iocinif  30506  voliune  31490  signstfvneq0  31844  lfuhgr3  32368  nosupbnd1lem5  33214  f1omptsnlem  34619  unccur  34877  matunitlindflem2  34891  stoweidlem15  42307  hoiqssbllem3  42913  vonioo  42971  vonicc  42974  gboge9  43936