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  3597  funfv  6910  2mpo0  7598  tfrlem7  8305  omword  8488  isinf  9154  fsuppunbi  9279  axdc3lem2  10345  supsrlem  11005  expclzlem  13990  expgt0  14002  expge0  14005  expge1  14006  swrdnd2  14562  resqrex  15157  rplpwr  16469  4sqlem19  16875  gexcl3  19466  thlle  21604  decpmataa0  22653  neindisj  23002  ptcmplem5  23941  tsmsxplem1  24038  tsmsxplem2  24039  elovolmr  25375  itgsubst  25954  logeftb  26490  logbchbase  26679  nosupbnd1lem5  27622  noinfbnd1lem5  27637  legov  28530  unopbd  31959  nmcoplb  31974  nmcfnlb  31998  nmopcoi  32039  an52ds  32395  an62ds  32396  an72ds  32397  an82ds  32398  iocinif  32725  1arithufdlem4  33485  r1plmhm  33543  r1pquslmic  33544  voliune  34202  signstfvneq0  34546  lfuhgr3  35103  f1omptsnlem  37320  unccur  37593  matunitlindflem2  37607  stoweidlem15  46006  hoiqssbllem3  46615  vonioo  46673  vonicc  46676  gboge9  47758  catprs  49006