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  8299  erinxp  8791  frrlem15  9739  fpwwe2lem11  10650  nqerf  10939  nqerid  10942  genpcl  11017  nqpr  11023  ltexprlem5  11049  psss  18668  psssdm2  18669  ismhmd  18894  idmhm  18903  resmhm2b  18931  prdspjmhm  18938  pwsdiagmhm  18940  pwsco1mhm  18941  pwsco2mhm  18942  frmdup1  18973  mhmfmhm  19188  isghmd  19352  ghmmhm  19353  idghm  19358  symgsubmefmndALT  19530  lactghmga  19532  frgpmhm  19892  frgpuplem  19899  mulgmhm  19954  isrhm2d  20632  idrhm  20636  pwsco1rhm  20652  pwsco2rhm  20653  subrgid  20735  issubrg2  20754  subsubrg  20760  pwsdiagrhm  20769  islmhmd  21223  reslmhm  21236  rngqiprngho  21506  issubassa  22082  subrgpsr  22192  mat1mhm  22706  mat1rhm  22707  scmatmhm  22756  scmatrhm  22757  mat2pmatmhm  22958  mat2pmatrhm  22959  m2cpmrhm  22971  pm2mpmhm  23045  pm2mprhm  23046  ptpjcn  23837  idnmhm  24980  pi1cpbl  25272  pi1grplem  25277  pi1xfr  25283  pi1coghm  25289  vitalilem1  25836  vitalilem3  25838  sltsd  28033  ssslts1  28038  ssslts2  28039  cgraer  29256  angmgmlem  29274  syl22anbrc  32935  fldgenfldext  34178  weiunso  37085  prjspertr  43451  prjspvs  43456  0prjspnrel  43473  nla0002  44264  nla0003  44265  clnbgrvtxel  48745  clnbgredg  48756