Theorem syl21anbrc 1357

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fprlem1  8274  erinxp  8766  frrlem15  9708  fpwwe2lem11  10592  nqerf  10881  nqerid  10884  genpcl  10959  nqpr  10965  ltexprlem5  10991  psss  18602  psssdm2  18603  ismhmd  18810  idmhm  18819  resmhm2b  18846  prdspjmhm  18853  pwsdiagmhm  18855  pwsco1mhm  18856  pwsco2mhm  18857  frmdup1  18888  mhmfmhm  19097  isghmd  19255  ghmmhm  19256  idghm  19261  symgsubmefmndALT  19433  lactghmga  19435  frgpmhm  19795  frgpuplem  19802  mulgmhm  19857  isrhm2d  20522  idrhm  20525  pwsco1rhm  20537  pwsco2rhm  20538  subrgid  20609  issubrg2  20628  subsubrg  20634  pwsdiagrhm  20643  islmhmd  21093  reslmhm  21106  rngqiprngho  21360  issubassa  21906  subrgpsr  22016  mat1mhm  22531  mat1rhm  22532  scmatmhm  22581  scmatrhm  22582  mat2pmatmhm  22780  mat2pmatrhm  22781  m2cpmrhm  22793  pm2mpmhm  22867  pm2mprhm  22868  ptpjcn  23658  idnmhm  24801  pi1cpbl  25093  pi1grplem  25098  pi1xfr  25104  pi1coghm  25110  vitalilem1  25657  vitalilem3  25659  sltsd  27848  ssslts1  27853  ssslts2  27854  syl22anbrc  32613  fldgenfldext  33925  weiunso  36786  prjspertr  43147  prjspvs  43152  0prjspnrel  43169  nla0002  43960  nla0003  43961  clnbgrvtxel  48411  clnbgredg  48422