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  6599  foimacnv  6840  respreima  7063  fpr  7156  fnprb  7212  curry1  8113  fnwelem  8141  frrlem12  8308  tfrlem10  8388  oawordeulem  8555  oelim2  8597  oaabs2  8651  omabs  8653  ssdomg  9020  limenpsi  9164  dffi2  9408  gruina  10896  recmulnq  11042  reclem2pr  11126  f1resfz0f1d  13920  climeu  15715  cosmul  16334  2ebits  16610  algcvgblem  16745  s1chn  18787  mgmideud  18832  ismgmid  18838  mndideuOLD  18928  ga0  19505  efgs1  19942  ricref  20741  pzriprnglem4  21783  psdmvr  22483  distopon  23308  dfac14  23930  ptcmplem5  24368  sszcld  25130  itg11  26005  axlowdimlem13  29525  nbusgredgeu  29940  1trld  30726  cycpmconjslem1  33708  1stmbfm  34885  2ndmbfm  34886  bnj150  35499  satfrel  36111  satf0n0  36122  mh-inf3sn  37310  bj-projval  37889  exidu1  38770  rngoideu  38817  refrelressn  39516  disjimeceqbi  39718  rfcnpre1  46005  fundcmpsurinjlem2  48450  gpgprismgr4cycllem11  49172