Theorem sylanbr 489

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  syl2anbr  496  funfv  6175  2mpt20  6780  tfrlem7  7366  omword  7537  isinf  8058  fsuppunbi  8179  axdc3lem2  9156  supsrlem  9811  expclzlem  12746  expgt0  12755  expge0  12758  expge1  12759  swrdnd2  13285  resqrex  13839  rplpwr  15114  isprm2lem  15232  4sqlem19  15505  gexcl3  17825  thlle  19860  decpmataa0  20392  neindisj  20731  ptcmplem5  21670  tsmsxplem1  21766  tsmsxplem2  21767  elovolmr  23051  itgsubst  23616  logeftb  24134  logbchbase  24309  legov  25280  constr2wlk  26128  unopbd  28258  nmcoplb  28273  nmcfnlb  28297  nmopcoi  28338  iocinif  28933  voliune  29619  signstfvneq0  29975  f1omptsnlem  32359  unccur  32562  matunitlindflem2  32576  stoweidlem15  38908  hoiqssbllem3  39514  vonioo  39573  vonicc  39576  gboage9  40186