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  6992  2mpo0  7691  tfrlem7  8416  omword  8603  isinf  9281  fsuppunbi  9405  axdc3lem2  10553  supsrlem  11220  expclzlem  14250  expgt0  14262  expge0  14265  expge1  14266  swrdnd2  14830  resqrex  15443  rplpwr  16758  4sqlem19  17167  gexcl3  19828  thlle  22030  matunitlindflem2  23022  decpmataa0  23113  neindisj  23462  ptcmplem5  24402  tsmsxplem1  24499  tsmsxplem2  24500  elovolmr  25824  itgsubst  26396  logeftb  26938  logbchbase  27126  nosupbnd1lem5  28096  noinfbnd1lem5  28111  legov  29075  lfuhgr3  29755  unopbd  32644  nmcoplb  32659  nmcfnlb  32683  nmopcoi  32724  an52ds  33121  an62ds  33122  an72ds  33123  an82ds  33124  iocinif  33440  1arithufdlem4  34146  r1plmhm  34208  r1pquslmic  34209  voliune  34929  signstfvneq0  35268  axprALT2  35815  weexenwe  35847  dfk12  36011  dfk22  36012  dfk32  36013  f1omptsnlem  38450  unccur  38717  stoweidlem15  47228  hoiqssbllem3  47837  vonioo  47895  vonicc  47898  gboge9  49065  catprs  50328