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  3584  funfv  6927  2mpo0  7616  tfrlem7  8322  omword  8505  isinf  9175  fsuppunbi  9302  axdc3lem2  10373  supsrlem  11034  expclzlem  14045  expgt0  14057  expge0  14060  expge1  14061  swrdnd2  14618  resqrex  15212  rplpwr  16527  4sqlem19  16934  gexcl3  19562  thlle  21677  decpmataa0  22733  neindisj  23082  ptcmplem5  24021  tsmsxplem1  24118  tsmsxplem2  24119  elovolmr  25443  itgsubst  26016  logeftb  26547  logbchbase  26735  nosupbnd1lem5  27676  noinfbnd1lem5  27691  legov  28653  unopbd  32086  nmcoplb  32101  nmcfnlb  32125  nmopcoi  32166  an52ds  32521  an62ds  32522  an72ds  32523  an82ds  32524  iocinif  32854  1arithufdlem4  33607  r1plmhm  33670  r1pquslmic  33671  voliune  34373  signstfvneq0  34716  axprALT2  35253  lfuhgr3  35302  f1omptsnlem  37652  unccur  37924  matunitlindflem2  37938  stoweidlem15  46443  hoiqssbllem3  47052  vonioo  47110  vonicc  47113  gboge9  48240  catprs  49486