Theorem sylanblrc 602

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fntp  6598  foimacnv  6839  respreima  7062  fpr  7155  fnprb  7211  curry1  8105  fnwelem  8133  frrlem12  8300  tfrlem10  8380  oawordeulem  8545  oelim2  8587  oaabs2  8641  omabs  8643  ssdomg  9010  limenpsi  9154  dffi2  9397  gruina  10831  recmulnq  10977  reclem2pr  11061  f1resfz0f1d  13852  climeu  15646  cosmul  16267  2ebits  16543  algcvgblem  16673  s1chn  18714  mgmideud  18759  ismgmid  18764  mndideuOLD  18854  ga0  19431  efgs1  19868  ricref  20665  pzriprnglem4  21703  psdmvr  22403  distopon  23228  dfac14  23850  ptcmplem5  24288  sszcld  25050  itg11  25925  axlowdimlem13  29419  nbusgredgeu  29834  1trld  30620  cycpmconjslem1  33602  1stmbfm  34779  2ndmbfm  34780  bnj150  35393  satfrel  35954  satf0n0  35965  mh-inf3sn  37169  bj-projval  37748  exidu1  38614  rngoideu  38661  refrelressn  39360  disjimeceqbi  39562  rfcnpre1  45861  fundcmpsurinjlem2  48307  gpgprismgr4cycllem11  49029