Theorem sylanbr 490

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  syl2anbr  497  funfv  6265  2mpt20  6882  tfrlem7  7479  omword  7650  isinf  8173  fsuppunbi  8296  axdc3lem2  9273  supsrlem  9932  expclzlem  12884  expgt0  12893  expge0  12896  expge1  12897  swrdnd2  13433  resqrex  13991  rplpwr  15276  4sqlem19  15667  gexcl3  18002  thlle  20041  decpmataa0  20573  neindisj  20921  ptcmplem5  21860  tsmsxplem1  21956  tsmsxplem2  21957  elovolmr  23244  itgsubst  23812  logeftb  24330  logbchbase  24509  legov  25480  unopbd  28874  nmcoplb  28889  nmcfnlb  28913  nmopcoi  28954  iocinif  29543  voliune  30292  signstfvneq0  30649  nosupbnd1lem5  31858  f1omptsnlem  33183  unccur  33392  matunitlindflem2  33406  stoweidlem15  40232  hoiqssbllem3  40838  vonioo  40896  vonicc  40899  gboge9  41652