Theorem syl21anbrc 1363

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fprlem1  8322  erinxp  8816  frrlem15  9765  fpwwe2lem11  10730  nqerf  11019  nqerid  11022  genpcl  11097  nqpr  11103  ltexprlem5  11129  psss  18760  psssdm2  18761  ismhmd  18987  idmhm  18996  resmhm2b  19024  prdspjmhm  19031  pwsdiagmhm  19033  pwsco1mhm  19034  pwsco2mhm  19035  frmdup1  19066  mhmfmhm  19281  isghmd  19445  ghmmhm  19446  idghm  19451  symgsubmefmndALT  19623  lactghmga  19625  frgpmhm  19985  frgpuplem  19992  mulgmhm  20047  isrhm2d  20727  idrhm  20731  pwsco1rhm  20747  pwsco2rhm  20748  subrgid  20831  issubrg2  20850  subsubrg  20856  pwsdiagrhm  20865  islmhmd  21320  reslmhm  21333  rngqiprngho  21605  issubassa  22181  subrgpsr  22291  mat1mhm  22805  mat1rhm  22806  scmatmhm  22855  scmatrhm  22856  mat2pmatmhm  23057  mat2pmatrhm  23058  m2cpmrhm  23070  pm2mpmhm  23144  pm2mprhm  23145  ptpjcn  23936  idnmhm  25079  pi1cpbl  25371  pi1grplem  25376  pi1xfr  25382  pi1coghm  25388  vitalilem1  25935  vitalilem3  25937  sltsd  28160  ssslts1  28165  ssslts2  28166  cgraer  29383  angmgmlem  29401  syl22anbrc  33104  fldgenfldext  34347  weiunso  37347  prjspertr  43727  prjspvs  43732  0prjspnrel  43757  nla0002  44519  nla0003  44520  clnbgrvtxel  49021  clnbgredg  49032