Theorem syl21anbrc 1342

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 233	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  fprlem1  8087  erinxp  8538  frrlem15  9446  fpwwe2lem11  10328  nqerf  10617  nqerid  10620  genpcl  10695  nqpr  10701  ltexprlem5  10727  psss  18213  psssdm2  18214  idmhm  18354  resmhm2b  18376  prdspjmhm  18382  pwsdiagmhm  18384  pwsco1mhm  18385  pwsco2mhm  18386  frmdup1  18418  mhmfmhm  18613  isghmd  18758  ghmmhm  18759  idghm  18764  symgsubmefmndALT  18926  lactghmga  18928  frgpmhm  19286  frgpuplem  19293  mulgmhm  19344  isrhm2d  19887  idrhm  19890  pwsco1rhm  19897  pwsco2rhm  19898  subrgid  19941  issubrg2  19959  subsubrg  19965  pwsdiagrhm  19973  islmhmd  20216  reslmhm  20229  issubassa  20983  subrgpsr  21098  mat1mhm  21541  mat1rhm  21542  scmatmhm  21591  scmatrhm  21592  mat2pmatmhm  21790  mat2pmatrhm  21791  m2cpmrhm  21803  pm2mpmhm  21877  pm2mprhm  21878  ptpjcn  22670  idnmhm  23824  pi1cpbl  24113  pi1grplem  24118  pi1xfr  24124  pi1coghm  24130  vitalilem1  24677  vitalilem3  24679  ssltd  33913  sssslt1  33916  sssslt2  33917  ismhmd  40164  prjspertr  40365  prjspvs  40370  0prjspnrel  40385