Theorem sylanbr 594

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anbr  611  rspc4v  3595  funfv  6960  2mpo0  7658  tfrlem7  8369  omword  8556  isinf  9234  fsuppunbi  9359  axdc3lem2  10500  supsrlem  11167  expclzlem  14194  expgt0  14206  expge0  14209  expge1  14210  swrdnd2  14772  resqrex  15384  rplpwr  16695  4sqlem19  17102  gexcl3  19762  thlle  21964  matunitlindflem2  22956  decpmataa0  23047  neindisj  23396  ptcmplem5  24336  tsmsxplem1  24433  tsmsxplem2  24434  elovolmr  25758  itgsubst  26330  logeftb  26874  logbchbase  27062  nosupbnd1lem5  28002  noinfbnd1lem5  28017  legov  28981  lfuhgr3  29661  unopbd  32550  nmcoplb  32565  nmcfnlb  32589  nmopcoi  32630  an52ds  32985  an62ds  32986  an72ds  32987  an82ds  32988  iocinif  33306  1arithufdlem4  34012  r1plmhm  34074  r1pquslmic  34075  voliune  34795  signstfvneq0  35135  axprALT2  35664  f1omptsnlem  38179  unccur  38446  stoweidlem15  46947  hoiqssbllem3  47556  vonioo  47614  vonicc  47617  gboge9  48784  catprs  50041