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  6537  foimacnv  6775  respreima  6993  fpr  7081  fnprb  7136  curry1  8028  fnwelem  8055  frrlem12  8221  tfrlem10  8300  oawordeulem  8463  oelim2  8504  oaabs2  8558  omabs  8560  ssdomg  8916  limenpsi  9059  dffi2  9301  gruina  10700  recmulnq  10846  reclem2pr  10930  climeu  15449  cosmul  16069  2ebits  16345  algcvgblem  16475  ismgmid  18526  mndideu  18606  ga0  19164  efgs1  19601  pzriprnglem4  21375  psdmvr  22038  distopon  22866  dfac14  23487  ptcmplem5  23925  sszcld  24687  itg11  25573  axlowdimlem13  28886  nbusgredgeu  29298  1trld  30073  s1chn  32947  cycpmconjslem1  33091  1stmbfm  34241  2ndmbfm  34242  bnj150  34856  f1resfz0f1d  35104  satfrel  35357  satf0n0  35368  bj-projval  36987  exidu1  37853  rngoideu  37900  refrelressn  38518  rfcnpre1  45013  fundcmpsurinjlem2  47397  gpgprismgr4cycllem11  48103