Theorem sylanblrc 592

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fntp  6415  foimacnv  6632  respreima  6836  fpr  6916  fnprb  6971  curry1  7799  fnwelem  7825  wfrlem13  7967  tfrlem10  8023  oawordeulem  8180  oelim2  8221  oaabs2  8272  omabs  8274  ssdomg  8555  limenpsi  8692  dffi2  8887  gruina  10240  recmulnq  10386  reclem2pr  10470  climeu  14912  cosmul  15526  2ebits  15796  algcvgblem  15921  ismgmid  17875  mndideu  17922  ga0  18428  efgs1  18861  distopon  21605  dfac14  22226  ptcmplem5  22664  sszcld  23425  itg11  24292  axlowdimlem13  26740  nbusgredgeu  27148  1trld  27921  cycpmconjslem1  30796  1stmbfm  31518  2ndmbfm  31519  bnj150  32148  f1resfz0f1d  32361  satfrel  32614  satf0n0  32625  frrlem12  33134  bj-projval  34311  exidu1  35149  rngoideu  35196  rfcnpre1  41296  fundcmpsurinjlem2  43579