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  6547  foimacnv  6785  respreima  7004  fpr  7092  fnprb  7148  curry1  8044  fnwelem  8071  frrlem12  8237  tfrlem10  8316  oawordeulem  8479  oelim2  8520  oaabs2  8574  omabs  8576  ssdomg  8932  limenpsi  9076  dffi2  9332  gruina  10731  recmulnq  10877  reclem2pr  10961  climeu  15481  cosmul  16101  2ebits  16377  algcvgblem  16507  ismgmid  18558  mndideu  18638  ga0  19196  efgs1  19633  pzriprnglem4  21410  psdmvr  22073  distopon  22901  dfac14  23522  ptcmplem5  23960  sszcld  24723  itg11  25609  axlowdimlem13  28918  nbusgredgeu  29330  1trld  30105  s1chn  32971  cycpmconjslem1  33115  1stmbfm  34247  2ndmbfm  34248  bnj150  34862  f1resfz0f1d  35106  satfrel  35359  satf0n0  35370  bj-projval  36989  exidu1  37855  rngoideu  37902  refrelressn  38520  rfcnpre1  45017  fundcmpsurinjlem2  47403  gpgprismgr4cycllem11  48109