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  6495  foimacnv  6733  respreima  6943  fpr  7026  fnprb  7084  curry1  7944  fnwelem  7972  frrlem12  8113  wfrlem13OLD  8152  tfrlem10  8218  oawordeulem  8385  oelim2  8426  oaabs2  8479  omabs  8481  ssdomg  8786  limenpsi  8939  dffi2  9182  gruina  10574  recmulnq  10720  reclem2pr  10804  climeu  15264  cosmul  15882  2ebits  16154  algcvgblem  16282  ismgmid  18349  mndideu  18396  ga0  18904  efgs1  19341  distopon  22147  dfac14  22769  ptcmplem5  23207  sszcld  23980  itg11  24855  axlowdimlem13  27322  nbusgredgeu  27733  1trld  28506  cycpmconjslem1  31421  1stmbfm  32227  2ndmbfm  32228  bnj150  32856  f1resfz0f1d  33072  satfrel  33329  satf0n0  33340  bj-projval  35186  exidu1  36014  rngoideu  36061  rfcnpre1  42562  fundcmpsurinjlem2  44851