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  6601  foimacnv  6842  respreima  7065  fpr  7155  fnprb  7210  curry1  8101  fnwelem  8129  frrlem12  8296  tfrlem10  8376  oawordeulem  8541  oelim2  8583  oaabs2  8637  omabs  8639  ssdomg  8999  limenpsi  9143  dffi2  9386  gruina  10814  recmulnq  10960  reclem2pr  11044  f1resfz0f1d  13834  climeu  15626  cosmul  16247  2ebits  16523  algcvgblem  16653  s1chn  18694  ismgmid  18741  mndideu  18825  ga0  19392  efgs1  19829  ricref  20626  pzriprnglem4  21664  psdmvr  22362  distopon  23184  dfac14  23806  ptcmplem5  24244  sszcld  25006  itg11  25881  axlowdimlem13  29335  nbusgredgeu  29750  1trld  30536  cycpmconjslem1  33514  1stmbfm  34691  2ndmbfm  34692  bnj150  35305  satfrel  35872  satf0n0  35883  mh-inf3sn  37086  bj-projval  37665  exidu1  38540  rngoideu  38587  refrelressn  39286  disjimeceqbi  39488  rfcnpre1  45772  fundcmpsurinjlem2  48181  gpgprismgr4cycllem11  48903