Theorem sylanblrc 591

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 584	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  6559  foimacnv  6797  respreima  7018  fpr  7108  fnprb  7163  curry1  8054  fnwelem  8081  frrlem12  8247  tfrlem10  8326  oawordeulem  8489  oelim2  8531  oaabs2  8585  omabs  8587  ssdomg  8947  limenpsi  9090  dffi2  9336  gruina  10741  recmulnq  10887  reclem2pr  10971  climeu  15517  cosmul  16140  2ebits  16416  algcvgblem  16546  s1chn  18586  ismgmid  18633  mndideu  18713  ga0  19273  efgs1  19710  pzriprnglem4  21464  psdmvr  22135  distopon  22962  dfac14  23583  ptcmplem5  24021  sszcld  24783  itg11  25658  axlowdimlem13  29023  nbusgredgeu  29435  1trld  30212  cycpmconjslem1  33215  1stmbfm  34404  2ndmbfm  34405  bnj150  35018  f1resfz0f1d  35296  satfrel  35549  satf0n0  35560  mh-inf3sn  36724  bj-projval  37303  exidu1  38177  rngoideu  38224  refrelressn  38925  disjimeceqbi  39127  rfcnpre1  45450  fundcmpsurinjlem2  47859  gpgprismgr4cycllem11  48581