Theorem syl21anbrc 1345

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 514	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anbrc.4	. 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 234	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fprlem1  8242  erinxp  8728  frrlem15  9669  fpwwe2lem11  10552  nqerf  10841  nqerid  10844  genpcl  10919  nqpr  10925  ltexprlem5  10951  psss  18503  psssdm2  18504  ismhmd  18711  idmhm  18720  resmhm2b  18747  prdspjmhm  18754  pwsdiagmhm  18756  pwsco1mhm  18757  pwsco2mhm  18758  frmdup1  18789  mhmfmhm  18995  isghmd  19154  ghmmhm  19155  idghm  19160  symgsubmefmndALT  19332  lactghmga  19334  frgpmhm  19694  frgpuplem  19701  mulgmhm  19756  isrhm2d  20422  idrhm  20425  pwsco1rhm  20435  pwsco2rhm  20436  subrgid  20506  issubrg2  20525  subsubrg  20531  pwsdiagrhm  20540  islmhmd  20991  reslmhm  21004  rngqiprngho  21258  issubassa  21822  subrgpsr  21933  mat1mhm  22428  mat1rhm  22429  scmatmhm  22478  scmatrhm  22479  mat2pmatmhm  22677  mat2pmatrhm  22678  m2cpmrhm  22690  pm2mpmhm  22764  pm2mprhm  22765  ptpjcn  23555  idnmhm  24698  pi1cpbl  25000  pi1grplem  25005  pi1xfr  25011  pi1coghm  25017  vitalilem1  25565  vitalilem3  25567  sltsd  27764  ssslts1  27769  ssslts2  27770  syl22anbrc  32529  fldgenfldext  33825  weiunso  36660  prjspertr  42848  prjspvs  42853  0prjspnrel  42870  nla0002  43665  nla0003  43666  clnbgrvtxel  48075  clnbgredg  48086