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  3605  funfv  6930  2mpo0  7618  tfrlem7  8328  omword  8511  isinf  9183  isinfOLD  9184  fsuppunbi  9316  axdc3lem2  10380  supsrlem  11040  expclzlem  14024  expgt0  14036  expge0  14039  expge1  14040  swrdnd2  14596  resqrex  15192  rplpwr  16504  4sqlem19  16910  gexcl3  19501  thlle  21639  decpmataa0  22688  neindisj  23037  ptcmplem5  23976  tsmsxplem1  24073  tsmsxplem2  24074  elovolmr  25410  itgsubst  25989  logeftb  26525  logbchbase  26714  nosupbnd1lem5  27657  noinfbnd1lem5  27672  legov  28565  unopbd  31994  nmcoplb  32009  nmcfnlb  32033  nmopcoi  32074  an52ds  32430  an62ds  32431  an72ds  32432  an82ds  32433  iocinif  32754  1arithufdlem4  33511  r1plmhm  33568  r1pquslmic  33569  voliune  34212  signstfvneq0  34556  lfuhgr3  35100  f1omptsnlem  37317  unccur  37590  matunitlindflem2  37604  stoweidlem15  46006  hoiqssbllem3  46615  vonioo  46673  vonicc  46676  gboge9  47758  catprs  48993