Theorem syl21anbrc 1344

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  fprlem1  8287  erinxp  8787  frrlem15  9754  fpwwe2lem11  10638  nqerf  10927  nqerid  10930  genpcl  11005  nqpr  11011  ltexprlem5  11037  psss  18535  psssdm2  18536  ismhmd  18676  idmhm  18683  resmhm2b  18705  prdspjmhm  18712  pwsdiagmhm  18714  pwsco1mhm  18715  pwsco2mhm  18716  frmdup1  18747  mhmfmhm  18950  isghmd  19103  ghmmhm  19104  idghm  19109  symgsubmefmndALT  19273  lactghmga  19275  frgpmhm  19635  frgpuplem  19642  mulgmhm  19697  isrhm2d  20269  idrhm  20272  pwsco1rhm  20281  pwsco2rhm  20282  subrgid  20325  issubrg2  20343  subsubrg  20349  pwsdiagrhm  20358  islmhmd  20655  reslmhm  20668  issubassa  21427  subrgpsr  21545  mat1mhm  21993  mat1rhm  21994  scmatmhm  22043  scmatrhm  22044  mat2pmatmhm  22242  mat2pmatrhm  22243  m2cpmrhm  22255  pm2mpmhm  22329  pm2mprhm  22330  ptpjcn  23122  idnmhm  24278  pi1cpbl  24567  pi1grplem  24572  pi1xfr  24578  pi1coghm  24584  vitalilem1  25132  vitalilem3  25134  ssltd  27300  sssslt1  27304  sssslt2  27305  prjspertr  41435  prjspvs  41440  0prjspnrel  41457  nla0002  42263  nla0003  42264  rngqiprngho  46873