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  6594  foimacnv  6835  respreima  7058  fpr  7151  fnprb  7207  curry1  8101  fnwelem  8129  frrlem12  8296  tfrlem10  8376  oawordeulem  8541  oelim2  8583  oaabs2  8637  omabs  8639  ssdomg  9006  limenpsi  9150  dffi2  9393  gruina  10827  recmulnq  10973  reclem2pr  11057  f1resfz0f1d  13848  climeu  15642  cosmul  16261  2ebits  16537  algcvgblem  16667  s1chn  18708  mgmideud  18753  ismgmid  18758  mndideuOLD  18848  ga0  19425  efgs1  19862  ricref  20659  pzriprnglem4  21697  psdmvr  22397  distopon  23222  dfac14  23844  ptcmplem5  24282  sszcld  25044  itg11  25919  axlowdimlem13  29411  nbusgredgeu  29826  1trld  30612  cycpmconjslem1  33594  1stmbfm  34771  2ndmbfm  34772  bnj150  35385  satfrel  35946  satf0n0  35957  mh-inf3sn  37161  bj-projval  37740  exidu1  38606  rngoideu  38653  refrelressn  39352  disjimeceqbi  39554  rfcnpre1  45853  fundcmpsurinjlem2  48299  gpgprismgr4cycllem11  49021