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  6492  foimacnv  6730  respreima  6938  fpr  7021  fnprb  7079  curry1  7929  fnwelem  7957  frrlem12  8098  wfrlem13OLD  8137  tfrlem10  8203  oawordeulem  8362  oelim2  8403  oaabs2  8454  omabs  8456  ssdomg  8761  limenpsi  8913  dffi2  9152  gruina  10567  recmulnq  10713  reclem2pr  10797  climeu  15254  cosmul  15872  2ebits  16144  algcvgblem  16272  ismgmid  18339  mndideu  18386  ga0  18894  efgs1  19331  distopon  22137  dfac14  22759  ptcmplem5  23197  sszcld  23970  itg11  24845  axlowdimlem13  27312  nbusgredgeu  27723  1trld  28494  cycpmconjslem1  31409  1stmbfm  32215  2ndmbfm  32216  bnj150  32844  f1resfz0f1d  33060  satfrel  33317  satf0n0  33328  bj-projval  35174  exidu1  36002  rngoideu  36049  rfcnpre1  42524  fundcmpsurinjlem2  44812