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  6580  foimacnv  6820  respreima  7041  fpr  7129  fnprb  7185  curry1  8086  fnwelem  8113  frrlem12  8279  tfrlem10  8358  oawordeulem  8521  oelim2  8562  oaabs2  8616  omabs  8618  ssdomg  8974  limenpsi  9122  dffi2  9381  gruina  10778  recmulnq  10924  reclem2pr  11008  climeu  15528  cosmul  16148  2ebits  16424  algcvgblem  16554  ismgmid  18599  mndideu  18679  ga0  19237  efgs1  19672  pzriprnglem4  21401  psdmvr  22063  distopon  22891  dfac14  23512  ptcmplem5  23950  sszcld  24713  itg11  25599  axlowdimlem13  28888  nbusgredgeu  29300  1trld  30078  s1chn  32943  cycpmconjslem1  33118  1stmbfm  34258  2ndmbfm  34259  bnj150  34873  f1resfz0f1d  35108  satfrel  35361  satf0n0  35372  bj-projval  36991  exidu1  37857  rngoideu  37904  refrelressn  38522  rfcnpre1  45020  fundcmpsurinjlem2  47404  gpgprismgr4cycllem11  48099