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  6597  foimacnv  6835  respreima  7056  fpr  7144  fnprb  7200  curry1  8103  fnwelem  8130  frrlem12  8296  wfrlem13OLD  8335  tfrlem10  8401  oawordeulem  8566  oelim2  8607  oaabs2  8661  omabs  8663  ssdomg  9014  limenpsi  9166  dffi2  9435  gruina  10832  recmulnq  10978  reclem2pr  11062  climeu  15571  cosmul  16191  2ebits  16466  algcvgblem  16596  ismgmid  18643  mndideu  18723  ga0  19281  efgs1  19716  pzriprnglem4  21445  psdmvr  22107  distopon  22935  dfac14  23556  ptcmplem5  23994  sszcld  24757  itg11  25644  axlowdimlem13  28933  nbusgredgeu  29345  1trld  30123  s1chn  32990  cycpmconjslem1  33165  1stmbfm  34292  2ndmbfm  34293  bnj150  34907  f1resfz0f1d  35136  satfrel  35389  satf0n0  35400  bj-projval  37014  exidu1  37880  rngoideu  37927  refrelressn  38542  rfcnpre1  45043  fundcmpsurinjlem2  47413  gpgprismgr4cycllem11  48104