Theorem syl21anbrc 1346

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  8250  erinxp  8738  frrlem15  9681  fpwwe2lem11  10564  nqerf  10853  nqerid  10856  genpcl  10931  nqpr  10937  ltexprlem5  10963  psss  18546  psssdm2  18547  ismhmd  18754  idmhm  18763  resmhm2b  18790  prdspjmhm  18797  pwsdiagmhm  18799  pwsco1mhm  18800  pwsco2mhm  18801  frmdup1  18832  mhmfmhm  19041  isghmd  19200  ghmmhm  19201  idghm  19206  symgsubmefmndALT  19378  lactghmga  19380  frgpmhm  19740  frgpuplem  19747  mulgmhm  19802  isrhm2d  20466  idrhm  20469  pwsco1rhm  20479  pwsco2rhm  20480  subrgid  20550  issubrg2  20569  subsubrg  20575  pwsdiagrhm  20584  islmhmd  21034  reslmhm  21047  rngqiprngho  21301  issubassa  21847  subrgpsr  21956  mat1mhm  22449  mat1rhm  22450  scmatmhm  22499  scmatrhm  22500  mat2pmatmhm  22698  mat2pmatrhm  22699  m2cpmrhm  22711  pm2mpmhm  22785  pm2mprhm  22786  ptpjcn  23576  idnmhm  24719  pi1cpbl  25011  pi1grplem  25016  pi1xfr  25022  pi1coghm  25028  vitalilem1  25575  vitalilem3  25577  sltsd  27760  ssslts1  27765  ssslts2  27766  syl22anbrc  32525  fldgenfldext  33812  weiunso  36648  prjspertr  43038  prjspvs  43043  0prjspnrel  43060  nla0002  43851  nla0003  43852  clnbgrvtxel  48305  clnbgredg  48316