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  8279  erinxp  8764  frrlem15  9710  fpwwe2lem11  10594  nqerf  10883  nqerid  10886  genpcl  10961  nqpr  10967  ltexprlem5  10993  psss  18539  psssdm2  18540  ismhmd  18713  idmhm  18722  resmhm2b  18749  prdspjmhm  18756  pwsdiagmhm  18758  pwsco1mhm  18759  pwsco2mhm  18760  frmdup1  18791  mhmfmhm  18997  isghmd  19157  ghmmhm  19158  idghm  19163  symgsubmefmndALT  19333  lactghmga  19335  frgpmhm  19695  frgpuplem  19702  mulgmhm  19757  isrhm2d  20396  idrhm  20399  pwsco1rhm  20411  pwsco2rhm  20412  subrgid  20482  issubrg2  20501  subsubrg  20507  pwsdiagrhm  20516  islmhmd  20946  reslmhm  20959  rngqiprngho  21213  issubassa  21776  subrgpsr  21887  mat1mhm  22371  mat1rhm  22372  scmatmhm  22421  scmatrhm  22422  mat2pmatmhm  22620  mat2pmatrhm  22621  m2cpmrhm  22633  pm2mpmhm  22707  pm2mprhm  22708  ptpjcn  23498  idnmhm  24642  pi1cpbl  24944  pi1grplem  24949  pi1xfr  24955  pi1coghm  24961  vitalilem1  25509  vitalilem3  25511  ssltd  27703  sssslt1  27707  sssslt2  27708  syl22anbrc  32384  fldgenfldext  33663  weiunso  36454  prjspertr  42593  prjspvs  42598  0prjspnrel  42615  nla0002  43413  nla0003  43414  clnbgrvtxel  47830  clnbgredg  47840