Theorem sylanbr 577

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  syl2anbr  592  funfv  6525  2mpt20  7159  tfrlem7  7762  omword  7934  isinf  8461  fsuppunbi  8584  axdc3lem2  9608  supsrlem  10268  expclzlem  13202  expgt0  13211  expge0  13214  expge1  13215  swrdnd2  13750  resqrex  14398  rplpwr  15682  4sqlem19  16071  gexcl3  18386  thlle  20440  decpmataa0  20980  neindisj  21329  ptcmplem5  22268  tsmsxplem1  22364  tsmsxplem2  22365  elovolmr  23680  itgsubst  24249  logeftb  24767  logbchbase  24949  legov  25936  unopbd  29446  nmcoplb  29461  nmcfnlb  29485  nmopcoi  29526  iocinif  30107  voliune  30890  signstfvneq0  31250  nosupbnd1lem5  32447  f1omptsnlem  33779  unccur  34019  matunitlindflem2  34034  stoweidlem15  41163  hoiqssbllem3  41769  vonioo  41827  vonicc  41830  gboge9  42681