Theorem sylanbr 580

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

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

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 395

This theorem is referenced by:  syl2anbr  597  rspc4v  3626  funfv  6981  2mpo0  7667  tfrlem7  8405  omword  8592  isinf  9287  isinfOLD  9288  fsuppunbi  9425  axdc3lem2  10485  supsrlem  11145  expclzlem  14097  expgt0  14109  expge0  14112  expge1  14113  swrdnd2  14658  resqrex  15250  rplpwr  16554  4sqlem19  16960  gexcl3  19581  thlle  21690  thlleOLD  21691  decpmataa0  22758  neindisj  23109  ptcmplem5  24048  tsmsxplem1  24145  tsmsxplem2  24146  elovolmr  25493  itgsubst  26072  logeftb  26607  logbchbase  26796  nosupbnd1lem5  27739  noinfbnd1lem5  27754  legov  28509  unopbd  31945  nmcoplb  31960  nmcfnlb  31984  nmopcoi  32025  an52ds  32378  an62ds  32379  an72ds  32380  an82ds  32381  iocinif  32686  1arithufdlem4  33428  r1plmhm  33483  r1pquslmic  33484  voliune  34075  signstfvneq0  34431  lfuhgr3  34960  f1omptsnlem  37056  unccur  37317  matunitlindflem2  37331  stoweidlem15  45672  hoiqssbllem3  46281  vonioo  46339  vonicc  46342  gboge9  47372  catprs  48368