Theorem syl21anbrc 1345

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  fprlem1  8230  erinxp  8715  frrlem15  9650  fpwwe2lem11  10532  nqerf  10821  nqerid  10824  genpcl  10899  nqpr  10905  ltexprlem5  10931  psss  18486  psssdm2  18487  ismhmd  18694  idmhm  18703  resmhm2b  18730  prdspjmhm  18737  pwsdiagmhm  18739  pwsco1mhm  18740  pwsco2mhm  18741  frmdup1  18772  mhmfmhm  18978  isghmd  19138  ghmmhm  19139  idghm  19144  symgsubmefmndALT  19316  lactghmga  19318  frgpmhm  19678  frgpuplem  19685  mulgmhm  19740  isrhm2d  20405  idrhm  20408  pwsco1rhm  20418  pwsco2rhm  20419  subrgid  20489  issubrg2  20508  subsubrg  20514  pwsdiagrhm  20523  islmhmd  20974  reslmhm  20987  rngqiprngho  21241  issubassa  21805  subrgpsr  21916  mat1mhm  22400  mat1rhm  22401  scmatmhm  22450  scmatrhm  22451  mat2pmatmhm  22649  mat2pmatrhm  22650  m2cpmrhm  22662  pm2mpmhm  22736  pm2mprhm  22737  ptpjcn  23527  idnmhm  24670  pi1cpbl  24972  pi1grplem  24977  pi1xfr  24983  pi1coghm  24989  vitalilem1  25537  vitalilem3  25539  ssltd  27732  sssslt1  27737  sssslt2  27738  syl22anbrc  32432  fldgenfldext  33679  weiunso  36506  prjspertr  42644  prjspvs  42649  0prjspnrel  42666  nla0002  43463  nla0003  43464  clnbgrvtxel  47866  clnbgredg  47877