Theorem sylanblrc 590

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fntp  6627  foimacnv  6865  respreima  7086  fpr  7174  fnprb  7228  curry1  8129  fnwelem  8156  frrlem12  8322  wfrlem13OLD  8361  tfrlem10  8427  oawordeulem  8592  oelim2  8633  oaabs2  8687  omabs  8689  ssdomg  9040  limenpsi  9192  dffi2  9463  gruina  10858  recmulnq  11004  reclem2pr  11088  climeu  15591  cosmul  16209  2ebits  16484  algcvgblem  16614  ismgmid  18678  mndideu  18758  ga0  19316  efgs1  19753  pzriprnglem4  21495  psdmvr  22173  distopon  23004  dfac14  23626  ptcmplem5  24064  sszcld  24839  itg11  25726  axlowdimlem13  28969  nbusgredgeu  29383  1trld  30161  s1chn  33000  cycpmconjslem1  33174  1stmbfm  34262  2ndmbfm  34263  bnj150  34890  f1resfz0f1d  35119  satfrel  35372  satf0n0  35383  bj-projval  36997  exidu1  37863  rngoideu  37910  refrelressn  38525  rfcnpre1  45024  fundcmpsurinjlem2  47386