Theorem sylanbr 589

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 587	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397

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 398

This theorem is referenced by:  syl2anbr  606  rspc4v  3582  funfv  6918  2mpo0  7609  tfrlem7  8316  omword  8499  isinf  9169  fsuppunbi  9296  axdc3lem2  10368  supsrlem  11029  expclzlem  14040  expgt0  14052  expge0  14055  expge1  14056  swrdnd2  14613  resqrex  15207  rplpwr  16522  4sqlem19  16929  gexcl3  19557  thlle  21676  decpmataa0  22755  neindisj  23104  ptcmplem5  24043  tsmsxplem1  24140  tsmsxplem2  24141  elovolmr  25465  itgsubst  26038  logeftb  26569  logbchbase  26757  nosupbnd1lem5  27698  noinfbnd1lem5  27713  legov  28675  unopbd  32108  nmcoplb  32123  nmcfnlb  32147  nmopcoi  32188  an52ds  32543  an62ds  32544  an72ds  32545  an82ds  32546  iocinif  32877  1arithufdlem4  33642  r1plmhm  33705  r1pquslmic  33706  voliune  34425  signstfvneq0  34768  axprALT2  35305  lfuhgr3  35363  f1omptsnlem  37713  unccur  37985  matunitlindflem2  37999  stoweidlem15  46472  hoiqssbllem3  47081  vonioo  47139  vonicc  47142  gboge9  48269  catprs  49515