Theorem syl21anbrc 1361

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fprlem1  8285  erinxp  8777  frrlem15  9717  fpwwe2lem11  10614  nqerf  10903  nqerid  10906  genpcl  10981  nqpr  10987  ltexprlem5  11013  psss  18624  psssdm2  18625  ismhmd  18832  idmhm  18841  resmhm2b  18869  prdspjmhm  18876  pwsdiagmhm  18878  pwsco1mhm  18879  pwsco2mhm  18880  frmdup1  18911  mhmfmhm  19119  isghmd  19283  ghmmhm  19284  idghm  19289  symgsubmefmndALT  19461  lactghmga  19463  frgpmhm  19823  frgpuplem  19830  mulgmhm  19885  isrhm2d  20557  idrhm  20560  pwsco1rhm  20572  pwsco2rhm  20573  subrgid  20646  issubrg2  20665  subsubrg  20671  pwsdiagrhm  20680  islmhmd  21126  reslmhm  21139  rngqiprngho  21402  issubassa  21974  subrgpsr  22084  mat1mhm  22598  mat1rhm  22599  scmatmhm  22648  scmatrhm  22649  mat2pmatmhm  22847  mat2pmatrhm  22848  m2cpmrhm  22860  pm2mpmhm  22934  pm2mprhm  22935  ptpjcn  23725  idnmhm  24868  pi1cpbl  25160  pi1grplem  25165  pi1xfr  25171  pi1coghm  25177  vitalilem1  25724  vitalilem3  25726  sltsd  27915  ssslts1  27920  ssslts2  27921  syl22anbrc  32711  fldgenfldext  33970  weiunso  36834  prjspertr  43194  prjspvs  43199  0prjspnrel  43216  nla0002  44007  nla0003  44008  clnbgrvtxel  48450  clnbgredg  48461