Theorem sylanblrc 601

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 594	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fntp  6595  foimacnv  6836  respreima  7059  fpr  7149  fnprb  7204  curry1  8095  fnwelem  8123  frrlem12  8290  tfrlem10  8370  oawordeulem  8535  oelim2  8577  oaabs2  8631  omabs  8633  ssdomg  8993  limenpsi  9136  dffi2  9379  gruina  10799  recmulnq  10945  reclem2pr  11029  climeu  15602  cosmul  16225  2ebits  16501  algcvgblem  16631  s1chn  18672  ismgmid  18719  mndideu  18799  ga0  19364  efgs1  19801  pzriprnglem4  21599  psdmvr  22297  distopon  23119  dfac14  23740  ptcmplem5  24178  sszcld  24940  itg11  25815  axlowdimlem13  29241  nbusgredgeu  29653  1trld  30430  cycpmconjslem1  33411  1stmbfm  34591  2ndmbfm  34592  bnj150  35205  f1resfz0f1d  35500  satfrel  35754  satf0n0  35765  mh-inf3sn  36938  bj-projval  37516  exidu1  38390  rngoideu  38437  refrelressn  39138  disjimeceqbi  39340  rfcnpre1  45626  fundcmpsurinjlem2  48032  gpgprismgr4cycllem11  48754