Theorem sylanbr 593

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anbr  610  rspc4v  3608  funfv  6969  2mpo0  7660  tfrlem7  8370  omword  8555  isinf  9225  fsuppunbi  9349  axdc3lem2  10435  supsrlem  11096  expclzlem  14119  expgt0  14131  expge0  14134  expge1  14135  swrdnd2  14693  resqrex  15301  rplpwr  16616  4sqlem19  17023  gexcl3  19657  thlle  21816  decpmataa0  22894  neindisj  23243  ptcmplem5  24182  tsmsxplem1  24279  tsmsxplem2  24280  elovolmr  25604  itgsubst  26177  logeftb  26714  logbchbase  26902  nosupbnd1lem5  27842  noinfbnd1lem5  27857  legov  28820  unopbd  32308  nmcoplb  32323  nmcfnlb  32347  nmopcoi  32388  an52ds  32743  an62ds  32744  an72ds  32745  an82ds  32746  iocinif  33067  1arithufdlem4  33782  r1plmhm  33844  r1pquslmic  33845  voliune  34564  signstfvneq0  34904  axprALT2  35446  lfuhgr3  35545  f1omptsnlem  37905  unccur  38177  matunitlindflem2  38191  stoweidlem15  46656  hoiqssbllem3  47265  vonioo  47323  vonicc  47326  gboge9  48453  catprs  49709