Theorem sylanblrc 590

Description: Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)

Hypotheses

Ref	Expression
sylanblrc.1	⊢ (𝜑 → 𝜓)
sylanblrc.2	⊢ 𝜒
sylanblrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanblrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanblrc

Step	Hyp	Ref	Expression
1		sylanblrc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylanblrc.2	. . 3 ⊢ 𝜒
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
4		sylanblrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	1, 3, 4	sylanbrc 583	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  fntp  6537  foimacnv  6775  respreima  6994  fpr  7082  fnprb  7137  curry1  8029  fnwelem  8056  frrlem12  8222  tfrlem10  8301  oawordeulem  8464  oelim2  8505  oaabs2  8559  omabs  8561  ssdomg  8917  limenpsi  9060  dffi2  9302  gruina  10704  recmulnq  10850  reclem2pr  10934  climeu  15457  cosmul  16077  2ebits  16353  algcvgblem  16483  s1chn  18521  ismgmid  18568  mndideu  18648  ga0  19205  efgs1  19642  pzriprnglem4  21416  psdmvr  22079  distopon  22907  dfac14  23528  ptcmplem5  23966  sszcld  24728  itg11  25614  axlowdimlem13  28927  nbusgredgeu  29339  1trld  30114  cycpmconjslem1  33115  1stmbfm  34265  2ndmbfm  34266  bnj150  34880  f1resfz0f1d  35150  satfrel  35403  satf0n0  35414  bj-projval  37030  exidu1  37896  rngoideu  37943  refrelressn  38561  rfcnpre1  45056  fundcmpsurinjlem2  47430  gpgprismgr4cycllem11  48136