Theorem sylanblrc 596

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fntp  6546  foimacnv  6784  respreima  7007  fpr  7097  fnprb  7152  curry1  8043  fnwelem  8071  frrlem12  8237  tfrlem10  8316  oawordeulem  8479  oelim2  8521  oaabs2  8575  omabs  8577  ssdomg  8937  limenpsi  9080  dffi2  9326  gruina  10732  recmulnq  10878  reclem2pr  10962  climeu  15508  cosmul  16131  2ebits  16407  algcvgblem  16537  s1chn  18577  ismgmid  18624  mndideu  18704  ga0  19264  efgs1  19701  pzriprnglem4  21459  psdmvr  22157  distopon  22980  dfac14  23601  ptcmplem5  24039  sszcld  24801  itg11  25676  axlowdimlem13  29041  nbusgredgeu  29453  1trld  30230  cycpmconjslem1  33235  1stmbfm  34444  2ndmbfm  34445  bnj150  35058  f1resfz0f1d  35342  satfrel  35595  satf0n0  35606  mh-inf3sn  36770  bj-projval  37349  exidu1  38223  rngoideu  38270  refrelressn  38971  disjimeceqbi  39173  rfcnpre1  45467  fundcmpsurinjlem2  47874  gpgprismgr4cycllem11  48596