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  6553  foimacnv  6791  respreima  7011  fpr  7099  fnprb  7154  curry1  8046  fnwelem  8073  frrlem12  8239  tfrlem10  8318  oawordeulem  8481  oelim2  8523  oaabs2  8577  omabs  8579  ssdomg  8937  limenpsi  9080  dffi2  9326  gruina  10729  recmulnq  10875  reclem2pr  10959  climeu  15478  cosmul  16098  2ebits  16374  algcvgblem  16504  s1chn  18543  ismgmid  18590  mndideu  18670  ga0  19227  efgs1  19664  pzriprnglem4  21439  psdmvr  22112  distopon  22941  dfac14  23562  ptcmplem5  24000  sszcld  24762  itg11  25648  axlowdimlem13  29027  nbusgredgeu  29439  1trld  30217  cycpmconjslem1  33236  1stmbfm  34417  2ndmbfm  34418  bnj150  35032  f1resfz0f1d  35308  satfrel  35561  satf0n0  35572  bj-projval  37197  exidu1  38057  rngoideu  38104  refrelressn  38777  rfcnpre1  45264  fundcmpsurinjlem2  47645  gpgprismgr4cycllem11  48351