Theorem syl21anbrc 1351

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  fprlem1  8247  erinxp  8735  frrlem15  9679  fpwwe2lem11  10562  nqerf  10851  nqerid  10854  genpcl  10929  nqpr  10935  ltexprlem5  10961  psss  18544  psssdm2  18545  ismhmd  18752  idmhm  18761  resmhm2b  18788  prdspjmhm  18795  pwsdiagmhm  18797  pwsco1mhm  18798  pwsco2mhm  18799  frmdup1  18830  mhmfmhm  19039  isghmd  19198  ghmmhm  19199  idghm  19204  symgsubmefmndALT  19376  lactghmga  19378  frgpmhm  19738  frgpuplem  19745  mulgmhm  19800  isrhm2d  20465  idrhm  20468  pwsco1rhm  20480  pwsco2rhm  20481  subrgid  20552  issubrg2  20571  subsubrg  20577  pwsdiagrhm  20586  islmhmd  21036  reslmhm  21049  rngqiprngho  21303  issubassa  21849  subrgpsr  21959  mat1mhm  22474  mat1rhm  22475  scmatmhm  22524  scmatrhm  22525  mat2pmatmhm  22723  mat2pmatrhm  22724  m2cpmrhm  22736  pm2mpmhm  22810  pm2mprhm  22811  ptpjcn  23601  idnmhm  24744  pi1cpbl  25036  pi1grplem  25041  pi1xfr  25047  pi1coghm  25053  vitalilem1  25600  vitalilem3  25602  sltsd  27785  ssslts1  27790  ssslts2  27791  syl22anbrc  32550  fldgenfldext  33859  weiunso  36701  prjspertr  43062  prjspvs  43067  0prjspnrel  43084  nla0002  43875  nla0003  43876  clnbgrvtxel  48327  clnbgredg  48338