Theorem sylanblrc 593

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fntp  6430  foimacnv  6667  respreima  6875  fpr  6958  fnprb  7013  curry1  7861  fnwelem  7887  frrlem12  8027  wfrlem13  8056  tfrlem10  8112  oawordeulem  8271  oelim2  8312  oaabs2  8363  omabs  8365  ssdomg  8663  limenpsi  8810  dffi2  9028  gruina  10415  recmulnq  10561  reclem2pr  10645  climeu  15099  cosmul  15715  2ebits  15987  algcvgblem  16115  ismgmid  18109  mndideu  18156  ga0  18664  efgs1  19097  distopon  21866  dfac14  22487  ptcmplem5  22925  sszcld  23686  itg11  24560  axlowdimlem13  27017  nbusgredgeu  27426  1trld  28197  cycpmconjslem1  31112  1stmbfm  31911  2ndmbfm  31912  bnj150  32541  f1resfz0f1d  32757  satfrel  33014  satf0n0  33025  bj-projval  34880  exidu1  35708  rngoideu  35755  rfcnpre1  42187  fundcmpsurinjlem2  44478