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  6561  foimacnv  6799  respreima  7020  fpr  7108  fnprb  7164  curry1  8060  fnwelem  8087  frrlem12  8253  tfrlem10  8332  oawordeulem  8495  oelim2  8536  oaabs2  8590  omabs  8592  ssdomg  8948  limenpsi  9093  dffi2  9350  gruina  10747  recmulnq  10893  reclem2pr  10977  climeu  15497  cosmul  16117  2ebits  16393  algcvgblem  16523  ismgmid  18568  mndideu  18648  ga0  19206  efgs1  19641  pzriprnglem4  21370  psdmvr  22032  distopon  22860  dfac14  23481  ptcmplem5  23919  sszcld  24682  itg11  25568  axlowdimlem13  28857  nbusgredgeu  29269  1trld  30044  s1chn  32909  cycpmconjslem1  33084  1stmbfm  34224  2ndmbfm  34225  bnj150  34839  f1resfz0f1d  35074  satfrel  35327  satf0n0  35338  bj-projval  36957  exidu1  37823  rngoideu  37870  refrelressn  38488  rfcnpre1  44986  fundcmpsurinjlem2  47373  gpgprismgr4cycllem11  48068