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  3599  funfv  6969  2mpo0  7666  tfrlem7  8375  omword  8560  isinf  9238  fsuppunbi  9362  axdc3lem2  10456  supsrlem  11123  expclzlem  14149  expgt0  14161  expge0  14164  expge1  14165  swrdnd2  14727  resqrex  15339  rplpwr  16652  4sqlem19  17059  gexcl3  19715  thlle  21911  matunitlindflem2  22903  decpmataa0  22994  neindisj  23343  ptcmplem5  24283  tsmsxplem1  24380  tsmsxplem2  24381  elovolmr  25705  itgsubst  26278  logeftb  26818  logbchbase  27006  nosupbnd1lem5  27946  noinfbnd1lem5  27961  legov  28925  lfuhgr3  29593  unopbd  32482  nmcoplb  32497  nmcfnlb  32521  nmopcoi  32562  an52ds  32917  an62ds  32918  an72ds  32919  an82ds  32920  iocinif  33239  1arithufdlem4  33944  r1plmhm  34006  r1pquslmic  34007  voliune  34727  signstfvneq0  35067  axprALT2  35604  f1omptsnlem  38077  unccur  38344  stoweidlem15  46830  hoiqssbllem3  47439  vonioo  47497  vonicc  47500  gboge9  48667  catprs  49924