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  8356  erinxp  8850  frrlem15  9798  fpwwe2lem11  10765  nqerf  11054  nqerid  11057  genpcl  11132  nqpr  11138  ltexprlem5  11164  psss  18804  psssdm2  18805  ismhmd  19031  idmhm  19040  resmhm2b  19068  prdspjmhm  19075  pwsdiagmhm  19077  pwsco1mhm  19078  pwsco2mhm  19079  frmdup1  19110  mhmfmhm  19325  isghmd  19489  ghmmhm  19490  idghm  19495  symgsubmefmndALT  19668  lactghmga  19670  frgpmhm  20030  frgpuplem  20037  mulgmhm  20092  isrhm2d  20772  idrhm  20776  pwsco1rhm  20792  pwsco2rhm  20793  subrgid  20876  issubrg2  20895  subsubrg  20901  pwsdiagrhm  20910  islmhmd  21365  reslmhm  21378  rngqiprngho  21650  issubassa  22230  subrgpsr  22340  mat1mhm  22854  mat1rhm  22855  scmatmhm  22904  scmatrhm  22905  mat2pmatmhm  23106  mat2pmatrhm  23107  m2cpmrhm  23119  pm2mpmhm  23193  pm2mprhm  23194  ptpjcn  23985  idnmhm  25128  pi1cpbl  25420  pi1grplem  25425  pi1xfr  25431  pi1coghm  25437  vitalilem1  25984  vitalilem3  25986  sltsd  28211  ssslts1  28216  ssslts2  28217  cgraer  29434  angmgmlem  29452  syl22anbrc  33155  fldgenfldext  34411  weiunso  37469  prjspertr  43899  prjspvs  43904  0prjspnrel  43929  nla0002  44686  nla0003  44687  clnbgrvtxel  49200  clnbgredg  49211