Theorem sylanblrc 588

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  fntp  6608  foimacnv  6849  respreima  7066  fpr  7153  fnprb  7211  curry1  8092  fnwelem  8119  frrlem12  8284  wfrlem13OLD  8323  tfrlem10  8389  oawordeulem  8556  oelim2  8597  oaabs2  8650  omabs  8652  ssdomg  8998  limenpsi  9154  dffi2  9420  gruina  10815  recmulnq  10961  reclem2pr  11045  climeu  15503  cosmul  16120  2ebits  16392  algcvgblem  16518  ismgmid  18590  mndideu  18670  ga0  19203  efgs1  19644  pzriprnglem4  21253  distopon  22720  dfac14  23342  ptcmplem5  23780  sszcld  24553  itg11  25440  axlowdimlem13  28479  nbusgredgeu  28890  1trld  29662  cycpmconjslem1  32583  1stmbfm  33557  2ndmbfm  33558  bnj150  34185  f1resfz0f1d  34401  satfrel  34656  satf0n0  34667  bj-projval  36180  exidu1  37027  rngoideu  37074  refrelressn  37697  rfcnpre1  44005  fundcmpsurinjlem2  46365