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 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  8288  erinxp  8788  frrlem15  9755  fpwwe2lem11  10639  nqerf  10928  nqerid  10931  genpcl  11006  nqpr  11012  ltexprlem5  11038  psss  18538  psssdm2  18539  ismhmd  18709  idmhm  18718  resmhm2b  18740  prdspjmhm  18747  pwsdiagmhm  18749  pwsco1mhm  18750  pwsco2mhm  18751  frmdup1  18782  mhmfmhm  18985  isghmd  19140  ghmmhm  19141  idghm  19146  symgsubmefmndALT  19313  lactghmga  19315  frgpmhm  19675  frgpuplem  19682  mulgmhm  19737  isrhm2d  20379  idrhm  20382  pwsco1rhm  20394  pwsco2rhm  20395  subrgid  20464  issubrg2  20483  subsubrg  20489  pwsdiagrhm  20498  islmhmd  20795  reslmhm  20808  rngqiprngho  21063  issubassa  21641  subrgpsr  21759  mat1mhm  22207  mat1rhm  22208  scmatmhm  22257  scmatrhm  22258  mat2pmatmhm  22456  mat2pmatrhm  22457  m2cpmrhm  22469  pm2mpmhm  22543  pm2mprhm  22544  ptpjcn  23336  idnmhm  24492  pi1cpbl  24792  pi1grplem  24797  pi1xfr  24803  pi1coghm  24809  vitalilem1  25358  vitalilem3  25360  ssltd  27526  sssslt1  27530  sssslt2  27531  prjspertr  41650  prjspvs  41655  0prjspnrel  41672  nla0002  42478  nla0003  42479