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  6972  2mpo0  7670  tfrlem7  8391  omword  8578  isinf  9256  fsuppunbi  9381  axdc3lem2  10529  supsrlem  11196  expclzlem  14226  expgt0  14238  expge0  14241  expge1  14242  swrdnd2  14805  resqrex  15417  rplpwr  16732  4sqlem19  17141  gexcl3  19801  thlle  22003  matunitlindflem2  22995  decpmataa0  23086  neindisj  23435  ptcmplem5  24375  tsmsxplem1  24472  tsmsxplem2  24473  elovolmr  25797  itgsubst  26369  logeftb  26911  logbchbase  27099  nosupbnd1lem5  28069  noinfbnd1lem5  28084  legov  29048  lfuhgr3  29728  unopbd  32617  nmcoplb  32632  nmcfnlb  32656  nmopcoi  32697  an52ds  33052  an62ds  33053  an72ds  33054  an82ds  33055  iocinif  33373  1arithufdlem4  34079  r1plmhm  34141  r1pquslmic  34142  voliune  34862  signstfvneq0  35201  axprALT2  35734  weexenwe  35756  f1omptsnlem  38260  unccur  38527  stoweidlem15  47025  hoiqssbllem3  47634  vonioo  47692  vonicc  47695  gboge9  48862  catprs  50119