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  9732  fpwwe2lem11  10637  nqerf  10926  nqerid  10929  genpcl  11004  nqpr  11010  ltexprlem5  11036  psss  18653  psssdm2  18654  ismhmd  18867  idmhm  18876  resmhm2b  18904  prdspjmhm  18911  pwsdiagmhm  18913  pwsco1mhm  18914  pwsco2mhm  18915  frmdup1  18946  mhmfmhm  19154  isghmd  19318  ghmmhm  19319  idghm  19324  symgsubmefmndALT  19496  lactghmga  19498  frgpmhm  19858  frgpuplem  19865  mulgmhm  19920  isrhm2d  20598  idrhm  20602  pwsco1rhm  20618  pwsco2rhm  20619  subrgid  20701  issubrg2  20720  subsubrg  20726  pwsdiagrhm  20735  islmhmd  21189  reslmhm  21202  rngqiprngho  21472  issubassa  22046  subrgpsr  22156  mat1mhm  22670  mat1rhm  22671  scmatmhm  22720  scmatrhm  22721  mat2pmatmhm  22919  mat2pmatrhm  22920  m2cpmrhm  22932  pm2mpmhm  23006  pm2mprhm  23007  ptpjcn  23797  idnmhm  24940  pi1cpbl  25232  pi1grplem  25237  pi1xfr  25243  pi1coghm  25249  vitalilem1  25796  vitalilem3  25798  sltsd  27990  ssslts1  27995  ssslts2  27996  syl22anbrc  32835  fldgenfldext  34081  weiunso  37010  prjspertr  43370  prjspvs  43375  0prjspnrel  43392  nla0002  44183  nla0003  44184  clnbgrvtxel  48627  clnbgredg  48638