Theorem sylanbr 593

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

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

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 401

This theorem is used by:  syl2anbr  610  rspc4v  3600  funfv  6968  2mpo0  7661  tfrlem7  8368  omword  8553  isinf  9223  fsuppunbi  9347  axdc3lem2  10441  supsrlem  11102  expclzlem  14126  expgt0  14138  expge0  14141  expge1  14142  swrdnd2  14700  resqrex  15308  rplpwr  16622  4sqlem19  17029  gexcl3  19663  thlle  21858  decpmataa0  22936  neindisj  23285  ptcmplem5  24224  tsmsxplem1  24321  tsmsxplem2  24322  elovolmr  25646  itgsubst  26219  logeftb  26759  logbchbase  26947  nosupbnd1lem5  27887  noinfbnd1lem5  27902  legov  28865  unopbd  32378  nmcoplb  32393  nmcfnlb  32417  nmopcoi  32458  an52ds  32813  an62ds  32814  an72ds  32815  an82ds  32816  iocinif  33137  1arithufdlem4  33846  r1plmhm  33908  r1pquslmic  33909  voliune  34628  signstfvneq0  34968  axprALT2  35512  lfuhgr3  35620  f1omptsnlem  38010  unccur  38282  matunitlindflem2  38296  stoweidlem15  46757  hoiqssbllem3  47366  vonioo  47424  vonicc  47427  gboge9  48557  catprs  49817