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  6553  foimacnv  6791  respreima  7012  fpr  7101  fnprb  7156  curry1  8047  fnwelem  8074  frrlem12  8240  tfrlem10  8319  oawordeulem  8482  oelim2  8524  oaabs2  8578  omabs  8580  ssdomg  8940  limenpsi  9083  dffi2  9329  gruina  10732  recmulnq  10878  reclem2pr  10962  climeu  15508  cosmul  16131  2ebits  16407  algcvgblem  16537  s1chn  18577  ismgmid  18624  mndideu  18704  ga0  19264  efgs1  19701  pzriprnglem4  21474  psdmvr  22145  distopon  22972  dfac14  23593  ptcmplem5  24031  sszcld  24793  itg11  25668  axlowdimlem13  29037  nbusgredgeu  29449  1trld  30227  cycpmconjslem1  33230  1stmbfm  34420  2ndmbfm  34421  bnj150  35034  f1resfz0f1d  35312  satfrel  35565  satf0n0  35576  mh-inf3sn  36740  bj-projval  37319  exidu1  38191  rngoideu  38238  refrelressn  38939  disjimeceqbi  39141  rfcnpre1  45468  fundcmpsurinjlem2  47871  gpgprismgr4cycllem11  48593