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  6597  foimacnv  6838  respreima  7061  fpr  7151  fnprb  7206  curry1  8095  fnwelem  8123  frrlem12  8290  tfrlem10  8370  oawordeulem  8535  oelim2  8577  oaabs2  8631  omabs  8633  ssdomg  8993  limenpsi  9136  dffi2  9379  gruina  10798  recmulnq  10944  reclem2pr  11028  climeu  15602  cosmul  16224  2ebits  16500  algcvgblem  16630  s1chn  18671  ismgmid  18718  mndideu  18798  ga0  19363  efgs1  19800  ricref  20596  pzriprnglem4  21634  psdmvr  22332  distopon  23154  dfac14  23775  ptcmplem5  24213  sszcld  24975  itg11  25850  axlowdimlem13  29304  nbusgredgeu  29716  1trld  30493  cycpmconjslem1  33474  1stmbfm  34650  2ndmbfm  34651  bnj150  35264  f1resfz0f1d  35605  satfrel  35859  satf0n0  35870  mh-inf3sn  37053  bj-projval  37632  exidu1  38507  rngoideu  38554  refrelressn  39253  disjimeceqbi  39455  rfcnpre1  45739  fundcmpsurinjlem2  48148  gpgprismgr4cycllem11  48870