Theorem sylanbr 583

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 581	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  600  rspc4v  3585  funfv  6923  2mpo0  7611  tfrlem7  8317  omword  8500  isinf  9170  fsuppunbi  9297  axdc3lem2  10368  supsrlem  11029  expclzlem  14040  expgt0  14052  expge0  14055  expge1  14056  swrdnd2  14613  resqrex  15207  rplpwr  16522  4sqlem19  16929  gexcl3  19557  thlle  21691  decpmataa0  22747  neindisj  23096  ptcmplem5  24035  tsmsxplem1  24132  tsmsxplem2  24133  elovolmr  25457  itgsubst  26030  logeftb  26564  logbchbase  26752  nosupbnd1lem5  27694  noinfbnd1lem5  27709  legov  28671  unopbd  32105  nmcoplb  32120  nmcfnlb  32144  nmopcoi  32185  an52ds  32540  an62ds  32541  an72ds  32542  an82ds  32543  iocinif  32873  1arithufdlem4  33626  r1plmhm  33689  r1pquslmic  33690  voliune  34393  signstfvneq0  34736  axprALT2  35273  lfuhgr3  35322  f1omptsnlem  37670  unccur  37942  matunitlindflem2  37956  stoweidlem15  46465  hoiqssbllem3  47074  vonioo  47132  vonicc  47135  gboge9  48256  catprs  49502