Theorem sylanblrc 599

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  fntp  6577  foimacnv  6819  respreima  7042  fpr  7132  fnprb  7187  curry1  8077  fnwelem  8105  frrlem12  8272  tfrlem10  8352  oawordeulem  8517  oelim2  8559  oaabs2  8613  omabs  8615  ssdomg  8975  limenpsi  9118  dffi2  9363  gruina  10770  recmulnq  10916  reclem2pr  11000  climeu  15573  cosmul  16196  2ebits  16472  algcvgblem  16602  s1chn  18643  ismgmid  18690  mndideu  18770  ga0  19329  efgs1  19766  pzriprnglem4  21524  psdmvr  22222  distopon  23045  dfac14  23666  ptcmplem5  24104  sszcld  24866  itg11  25741  axlowdimlem13  29112  nbusgredgeu  29524  1trld  30301  cycpmconjslem1  33295  1stmbfm  34518  2ndmbfm  34519  bnj150  35132  f1resfz0f1d  35425  satfrel  35678  satf0n0  35689  mh-inf3sn  36863  bj-projval  37442  exidu1  38316  rngoideu  38363  refrelressn  39064  disjimeceqbi  39266  rfcnpre1  45560  fundcmpsurinjlem2  47966  gpgprismgr4cycllem11  48688