Theorem sylanblrc 591

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 584	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  6561  foimacnv  6799  respreima  7020  fpr  7109  fnprb  7164  curry1  8056  fnwelem  8083  frrlem12  8249  tfrlem10  8328  oawordeulem  8491  oelim2  8533  oaabs2  8587  omabs  8589  ssdomg  8949  limenpsi  9092  dffi2  9338  gruina  10741  recmulnq  10887  reclem2pr  10971  climeu  15490  cosmul  16110  2ebits  16386  algcvgblem  16516  s1chn  18555  ismgmid  18602  mndideu  18682  ga0  19239  efgs1  19676  pzriprnglem4  21451  psdmvr  22124  distopon  22953  dfac14  23574  ptcmplem5  24012  sszcld  24774  itg11  25660  axlowdimlem13  29039  nbusgredgeu  29451  1trld  30229  cycpmconjslem1  33248  1stmbfm  34438  2ndmbfm  34439  bnj150  35052  f1resfz0f1d  35330  satfrel  35583  satf0n0  35594  bj-projval  37244  exidu1  38107  rngoideu  38154  refrelressn  38855  disjimeceqbi  39057  rfcnpre1  45379  fundcmpsurinjlem2  47759  gpgprismgr4cycllem11  48465