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  6604  foimacnv  6845  respreima  7068  fpr  7161  fnprb  7216  curry1  8119  fnwelem  8147  frrlem12  8320  tfrlem10  8400  oawordeulem  8567  oelim2  8609  oaabs2  8663  omabs  8665  ssdomg  9032  limenpsi  9176  dffi2  9420  gruina  10908  recmulnq  11054  reclem2pr  11138  f1resfz0f1d  13932  climeu  15729  cosmul  16348  2ebits  16624  algcvgblem  16759  s1chn  18801  mgmideud  18846  ismgmid  18852  mndideuOLD  18942  ga0  19519  efgs1  19956  ricref  20755  pzriprnglem4  21797  psdmvr  22497  distopon  23322  dfac14  23944  ptcmplem5  24382  sszcld  25144  itg11  26019  axlowdimlem13  29539  nbusgredgeu  29954  1trld  30740  cycpmconjslem1  33763  1stmbfm  34940  2ndmbfm  34941  bnj150  35554  soinfdom  35770  satfrel  36220  satf0n0  36231  cardprcr  36552  mh-inf3sn  37424  bj-projval  38003  exidu1  38897  rngoideu  38944  refrelressn  39643  disjimeceqbi  39845  hfstructhf  46137  rfcnpre1  46143  fundcmpsurinjlem2  48588  gpgprismgr4cycllem11  49310