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  6550  foimacnv  6788  respreima  7008  fpr  7096  fnprb  7151  curry1  8043  fnwelem  8070  frrlem12  8236  tfrlem10  8315  oawordeulem  8478  oelim2  8519  oaabs2  8573  omabs  8575  ssdomg  8933  limenpsi  9076  dffi2  9318  gruina  10720  recmulnq  10866  reclem2pr  10950  climeu  15469  cosmul  16089  2ebits  16365  algcvgblem  16495  s1chn  18534  ismgmid  18581  mndideu  18661  ga0  19218  efgs1  19655  pzriprnglem4  21430  psdmvr  22103  distopon  22932  dfac14  23553  ptcmplem5  23991  sszcld  24753  itg11  25639  axlowdimlem13  28953  nbusgredgeu  29365  1trld  30143  cycpmconjslem1  33164  1stmbfm  34345  2ndmbfm  34346  bnj150  34960  f1resfz0f1d  35230  satfrel  35483  satf0n0  35494  bj-projval  37113  exidu1  37969  rngoideu  38016  refrelressn  38689  rfcnpre1  45180  fundcmpsurinjlem2  47561  gpgprismgr4cycllem11  48267