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  6629  foimacnv  6866  respreima  7086  fpr  7174  fnprb  7228  curry1  8128  fnwelem  8155  frrlem12  8321  wfrlem13OLD  8360  tfrlem10  8426  oawordeulem  8591  oelim2  8632  oaabs2  8686  omabs  8688  ssdomg  9039  limenpsi  9191  dffi2  9461  gruina  10856  recmulnq  11002  reclem2pr  11086  climeu  15588  cosmul  16206  2ebits  16481  algcvgblem  16611  ismgmid  18691  mndideu  18771  ga0  19329  efgs1  19768  pzriprnglem4  21513  distopon  23020  dfac14  23642  ptcmplem5  24080  sszcld  24853  itg11  25740  axlowdimlem13  28984  nbusgredgeu  29398  1trld  30171  cycpmconjslem1  33157  1stmbfm  34242  2ndmbfm  34243  bnj150  34869  f1resfz0f1d  35098  satfrel  35352  satf0n0  35363  bj-projval  36979  exidu1  37843  rngoideu  37890  refrelressn  38506  rfcnpre1  44957  fundcmpsurinjlem2  47324