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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 398

This theorem is referenced by:  syl2anbr  600  rspc4v  3631  funfv  6979  2mpo0  7655  tfrlem7  8383  omword  8570  isinf  9260  isinfOLD  9261  fsuppunbi  9384  axdc3lem2  10446  supsrlem  11106  expclzlem  14049  expgt0  14061  expge0  14064  expge1  14065  swrdnd2  14605  resqrex  15197  rplpwr  16499  4sqlem19  16896  gexcl3  19455  thlle  21251  thlleOLD  21252  decpmataa0  22270  neindisj  22621  ptcmplem5  23560  tsmsxplem1  23657  tsmsxplem2  23658  elovolmr  24993  itgsubst  25566  logeftb  26092  logbchbase  26276  nosupbnd1lem5  27215  noinfbnd1lem5  27230  legov  27836  unopbd  31268  nmcoplb  31283  nmcfnlb  31307  nmopcoi  31348  iocinif  31992  voliune  33227  signstfvneq0  33583  lfuhgr3  34110  f1omptsnlem  36217  unccur  36471  matunitlindflem2  36485  stoweidlem15  44731  hoiqssbllem3  45340  vonioo  45398  vonicc  45401  gboge9  46432  catprs  47631