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  8304  erinxp  8810  frrlem15  9776  fpwwe2lem11  10660  nqerf  10949  nqerid  10952  genpcl  11027  nqpr  11033  ltexprlem5  11059  psss  18595  psssdm2  18596  ismhmd  18769  idmhm  18778  resmhm2b  18805  prdspjmhm  18812  pwsdiagmhm  18814  pwsco1mhm  18815  pwsco2mhm  18816  frmdup1  18847  mhmfmhm  19053  isghmd  19213  ghmmhm  19214  idghm  19219  symgsubmefmndALT  19389  lactghmga  19391  frgpmhm  19751  frgpuplem  19758  mulgmhm  19813  isrhm2d  20452  idrhm  20455  pwsco1rhm  20467  pwsco2rhm  20468  subrgid  20538  issubrg2  20557  subsubrg  20563  pwsdiagrhm  20572  islmhmd  21002  reslmhm  21015  rngqiprngho  21269  issubassa  21832  subrgpsr  21943  mat1mhm  22427  mat1rhm  22428  scmatmhm  22477  scmatrhm  22478  mat2pmatmhm  22676  mat2pmatrhm  22677  m2cpmrhm  22689  pm2mpmhm  22763  pm2mprhm  22764  ptpjcn  23554  idnmhm  24698  pi1cpbl  25000  pi1grplem  25005  pi1xfr  25011  pi1coghm  25017  vitalilem1  25566  vitalilem3  25568  ssltd  27760  sssslt1  27764  sssslt2  27765  syl22anbrc  32441  fldgenfldext  33714  weiunso  36489  prjspertr  42603  prjspvs  42608  0prjspnrel  42625  nla0002  43423  nla0003  43424  clnbgrvtxel  47823  clnbgredg  47833