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

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 398

This theorem is referenced by:  fntp  6610  foimacnv  6851  respreima  7068  fpr  7152  fnprb  7210  curry1  8090  fnwelem  8117  frrlem12  8282  wfrlem13OLD  8321  tfrlem10  8387  oawordeulem  8554  oelim2  8595  oaabs2  8648  omabs  8650  ssdomg  8996  limenpsi  9152  dffi2  9418  gruina  10813  recmulnq  10959  reclem2pr  11043  climeu  15499  cosmul  16116  2ebits  16388  algcvgblem  16514  ismgmid  18584  mndideu  18636  ga0  19162  efgs1  19603  distopon  22500  dfac14  23122  ptcmplem5  23560  sszcld  24333  itg11  25208  axlowdimlem13  28212  nbusgredgeu  28623  1trld  29395  cycpmconjslem1  32313  1stmbfm  33259  2ndmbfm  33260  bnj150  33887  f1resfz0f1d  34103  satfrel  34358  satf0n0  34369  bj-projval  35877  exidu1  36724  rngoideu  36771  refrelressn  37394  rfcnpre1  43703  fundcmpsurinjlem2  46067  pzriprnglem4  46808