Theorem syl21anbrc 1363

Description: Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)

Hypotheses

Ref	Expression
syl21anbrc.1	⊢ (𝜑 → 𝜓)
syl21anbrc.2	⊢ (𝜑 → 𝜒)
syl21anbrc.3	⊢ (𝜑 → 𝜃)
syl21anbrc.4	⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))

Assertion

Ref	Expression
syl21anbrc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anbrc

Step	Hyp	Ref	Expression
1		syl21anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl21anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl21anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca31 523	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anbrc.4	. 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 237	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fprlem1  8298  erinxp  8790  frrlem15  9730  fpwwe2lem11  10627  nqerf  10916  nqerid  10919  genpcl  10994  nqpr  11000  ltexprlem5  11026  psss  18637  psssdm2  18638  ismhmd  18845  idmhm  18854  resmhm2b  18882  prdspjmhm  18889  pwsdiagmhm  18891  pwsco1mhm  18892  pwsco2mhm  18893  frmdup1  18924  mhmfmhm  19132  isghmd  19296  ghmmhm  19297  idghm  19302  symgsubmefmndALT  19474  lactghmga  19476  frgpmhm  19836  frgpuplem  19843  mulgmhm  19898  isrhm2d  20570  idrhm  20573  pwsco1rhm  20585  pwsco2rhm  20586  subrgid  20659  issubrg2  20678  subsubrg  20684  pwsdiagrhm  20693  islmhmd  21141  reslmhm  21154  rngqiprngho  21424  issubassa  21998  subrgpsr  22108  mat1mhm  22622  mat1rhm  22623  scmatmhm  22672  scmatrhm  22673  mat2pmatmhm  22871  mat2pmatrhm  22872  m2cpmrhm  22884  pm2mpmhm  22958  pm2mprhm  22959  ptpjcn  23749  idnmhm  24892  pi1cpbl  25184  pi1grplem  25189  pi1xfr  25195  pi1coghm  25201  vitalilem1  25748  vitalilem3  25750  sltsd  27942  ssslts1  27947  ssslts2  27948  syl22anbrc  32787  fldgenfldext  34039  weiunso  36958  prjspertr  43320  prjspvs  43325  0prjspnrel  43342  nla0002  44133  nla0003  44134  clnbgrvtxel  48577  clnbgredg  48588