Theorem sylanblrc 589

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 582	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  6639  foimacnv  6879  respreima  7099  fpr  7188  fnprb  7245  curry1  8145  fnwelem  8172  frrlem12  8338  wfrlem13OLD  8377  tfrlem10  8443  oawordeulem  8610  oelim2  8651  oaabs2  8705  omabs  8707  ssdomg  9060  limenpsi  9218  dffi2  9492  gruina  10887  recmulnq  11033  reclem2pr  11117  climeu  15601  cosmul  16221  2ebits  16493  algcvgblem  16624  ismgmid  18703  mndideu  18783  ga0  19338  efgs1  19777  pzriprnglem4  21518  distopon  23025  dfac14  23647  ptcmplem5  24085  sszcld  24858  itg11  25745  axlowdimlem13  28987  nbusgredgeu  29401  1trld  30174  cycpmconjslem1  33147  1stmbfm  34225  2ndmbfm  34226  bnj150  34852  f1resfz0f1d  35081  satfrel  35335  satf0n0  35346  bj-projval  36962  exidu1  37816  rngoideu  37863  refrelressn  38480  rfcnpre1  44919  fundcmpsurinjlem2  47273