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  6577  foimacnv  6817  respreima  7038  fpr  7126  fnprb  7182  curry1  8083  fnwelem  8110  frrlem12  8276  tfrlem10  8355  oawordeulem  8518  oelim2  8559  oaabs2  8613  omabs  8615  ssdomg  8971  limenpsi  9116  dffi2  9374  gruina  10771  recmulnq  10917  reclem2pr  11001  climeu  15521  cosmul  16141  2ebits  16417  algcvgblem  16547  ismgmid  18592  mndideu  18672  ga0  19230  efgs1  19665  pzriprnglem4  21394  psdmvr  22056  distopon  22884  dfac14  23505  ptcmplem5  23943  sszcld  24706  itg11  25592  axlowdimlem13  28881  nbusgredgeu  29293  1trld  30071  s1chn  32936  cycpmconjslem1  33111  1stmbfm  34251  2ndmbfm  34252  bnj150  34866  f1resfz0f1d  35101  satfrel  35354  satf0n0  35365  bj-projval  36984  exidu1  37850  rngoideu  37897  refrelressn  38515  rfcnpre1  45013  fundcmpsurinjlem2  47400  gpgprismgr4cycllem11  48095