Theorem syl21anbrc 1343

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

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

This theorem is referenced by:  fprlem1  8116  erinxp  8580  frrlem15  9515  fpwwe2lem11  10397  nqerf  10686  nqerid  10689  genpcl  10764  nqpr  10770  ltexprlem5  10796  psss  18298  psssdm2  18299  idmhm  18439  resmhm2b  18461  prdspjmhm  18467  pwsdiagmhm  18469  pwsco1mhm  18470  pwsco2mhm  18471  frmdup1  18503  mhmfmhm  18698  isghmd  18843  ghmmhm  18844  idghm  18849  symgsubmefmndALT  19011  lactghmga  19013  frgpmhm  19371  frgpuplem  19378  mulgmhm  19429  isrhm2d  19972  idrhm  19975  pwsco1rhm  19982  pwsco2rhm  19983  subrgid  20026  issubrg2  20044  subsubrg  20050  pwsdiagrhm  20058  islmhmd  20301  reslmhm  20314  issubassa  21073  subrgpsr  21188  mat1mhm  21633  mat1rhm  21634  scmatmhm  21683  scmatrhm  21684  mat2pmatmhm  21882  mat2pmatrhm  21883  m2cpmrhm  21895  pm2mpmhm  21969  pm2mprhm  21970  ptpjcn  22762  idnmhm  23918  pi1cpbl  24207  pi1grplem  24212  pi1xfr  24218  pi1coghm  24224  vitalilem1  24772  vitalilem3  24774  ssltd  33986  sssslt1  33989  sssslt2  33990  ismhmd  40238  prjspertr  40444  prjspvs  40449  0prjspnrel  40464