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 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fntp  6609  foimacnv  6850  respreima  7067  fpr  7151  fnprb  7209  curry1  8089  fnwelem  8116  frrlem12  8281  wfrlem13OLD  8320  tfrlem10  8386  oawordeulem  8553  oelim2  8594  oaabs2  8647  omabs  8649  ssdomg  8995  limenpsi  9151  dffi2  9417  gruina  10812  recmulnq  10958  reclem2pr  11042  climeu  15498  cosmul  16115  2ebits  16387  algcvgblem  16513  ismgmid  18583  mndideu  18635  ga0  19161  efgs1  19602  distopon  22499  dfac14  23121  ptcmplem5  23559  sszcld  24332  itg11  25207  axlowdimlem13  28209  nbusgredgeu  28620  1trld  29392  cycpmconjslem1  32308  1stmbfm  33254  2ndmbfm  33255  bnj150  33882  f1resfz0f1d  34098  satfrel  34353  satf0n0  34364  bj-projval  35872  exidu1  36719  rngoideu  36766  refrelressn  37389  rfcnpre1  43693  fundcmpsurinjlem2  46057  pzriprnglem4  46798