Theorem sylanblrc 602

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fntp  6631  foimacnv  6872  respreima  7097  fpr  7190  fnprb  7245  curry1  8152  fnwelem  8180  frrlem12  8353  tfrlem10  8433  oawordeulem  8600  oelim2  8642  oaabs2  8696  omabs  8698  ssdomg  9065  limenpsi  9209  dffi2  9452  cardprcr  10099  gruina  10942  recmulnq  11088  reclem2pr  11172  f1resfz0f1d  13967  climeu  15766  cosmul  16385  2ebits  16661  algcvgblem  16796  s1chn  18844  mgmideud  18889  ismgmid  18895  mndideuOLD  18985  ga0  19563  efgs1  20000  ricref  20799  pzriprnglem4  21845  psdmvr  22545  distopon  23370  dfac14  23992  ptcmplem5  24430  sszcld  25192  itg11  26067  axlowdimlem13  29589  nbusgredgeu  30004  1trld  30790  cycpmconjslem1  33814  1stmbfm  35003  2ndmbfm  35004  bnj150  35617  soinfdom  35841  satfrel  36340  satf0n0  36351  mh-inf3sn  37545  bj-projval  38124  exidu1  39056  rngoideu  39103  refrelressn  39802  disjimeceqbi  40004  grpgimcanon  46192  hfstructhf  46297  rfcnpre1  46310  fundcmpsurinjlem2  48754  gpgprismgr4cycllem11  49476