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  8311  erinxp  8805  frrlem15  9754  fpwwe2lem11  10719  nqerf  11008  nqerid  11011  genpcl  11086  nqpr  11092  ltexprlem5  11118  psss  18747  psssdm2  18748  ismhmd  18974  idmhm  18983  resmhm2b  19011  prdspjmhm  19018  pwsdiagmhm  19020  pwsco1mhm  19021  pwsco2mhm  19022  frmdup1  19053  mhmfmhm  19268  isghmd  19432  ghmmhm  19433  idghm  19438  symgsubmefmndALT  19610  lactghmga  19612  frgpmhm  19972  frgpuplem  19979  mulgmhm  20034  isrhm2d  20714  idrhm  20718  pwsco1rhm  20734  pwsco2rhm  20735  subrgid  20818  issubrg2  20837  subsubrg  20843  pwsdiagrhm  20852  islmhmd  21307  reslmhm  21320  rngqiprngho  21592  issubassa  22168  subrgpsr  22278  mat1mhm  22792  mat1rhm  22793  scmatmhm  22842  scmatrhm  22843  mat2pmatmhm  23044  mat2pmatrhm  23045  m2cpmrhm  23057  pm2mpmhm  23131  pm2mprhm  23132  ptpjcn  23923  idnmhm  25066  pi1cpbl  25358  pi1grplem  25363  pi1xfr  25369  pi1coghm  25375  vitalilem1  25922  vitalilem3  25924  sltsd  28147  ssslts1  28152  ssslts2  28153  cgraer  29370  angmgmlem  29388  syl22anbrc  33049  fldgenfldext  34293  weiunso  37234  prjspertr  43613  prjspvs  43618  0prjspnrel  43643  nla0002  44409  nla0003  44410  clnbgrvtxel  48896  clnbgredg  48907