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 227	. 2 ⊢ (𝜑 → 𝜓)
3		sylanbr.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syl2anbr  599  funfv  6855  2mpo0  7518  tfrlem7  8214  omword  8401  isinf  9036  fsuppunbi  9149  axdc3lem2  10207  supsrlem  10867  expclzlem  13806  expgt0  13816  expge0  13819  expge1  13820  swrdnd2  14368  resqrex  14962  rplpwr  16267  4sqlem19  16664  gexcl3  19192  thlle  20903  thlleOLD  20904  decpmataa0  21917  neindisj  22268  ptcmplem5  23207  tsmsxplem1  23304  tsmsxplem2  23305  elovolmr  24640  itgsubst  25213  logeftb  25739  logbchbase  25921  legov  26946  unopbd  30377  nmcoplb  30392  nmcfnlb  30416  nmopcoi  30457  iocinif  31102  voliune  32197  signstfvneq0  32551  lfuhgr3  33081  nosupbnd1lem5  33915  noinfbnd1lem5  33930  f1omptsnlem  35507  unccur  35760  matunitlindflem2  35774  stoweidlem15  43556  hoiqssbllem3  44162  vonioo  44220  vonicc  44223  gboge9  45216  catprs  46292