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  8325  erinxp  8831  frrlem15  9797  fpwwe2lem11  10681  nqerf  10970  nqerid  10973  genpcl  11048  nqpr  11054  ltexprlem5  11080  psss  18625  psssdm2  18626  ismhmd  18799  idmhm  18808  resmhm2b  18835  prdspjmhm  18842  pwsdiagmhm  18844  pwsco1mhm  18845  pwsco2mhm  18846  frmdup1  18877  mhmfmhm  19083  isghmd  19243  ghmmhm  19244  idghm  19249  symgsubmefmndALT  19421  lactghmga  19423  frgpmhm  19783  frgpuplem  19790  mulgmhm  19845  isrhm2d  20487  idrhm  20490  pwsco1rhm  20502  pwsco2rhm  20503  subrgid  20573  issubrg2  20592  subsubrg  20598  pwsdiagrhm  20607  islmhmd  21038  reslmhm  21051  rngqiprngho  21313  issubassa  21887  subrgpsr  21998  mat1mhm  22490  mat1rhm  22491  scmatmhm  22540  scmatrhm  22541  mat2pmatmhm  22739  mat2pmatrhm  22740  m2cpmrhm  22752  pm2mpmhm  22826  pm2mprhm  22827  ptpjcn  23619  idnmhm  24775  pi1cpbl  25077  pi1grplem  25082  pi1xfr  25088  pi1coghm  25094  vitalilem1  25643  vitalilem3  25645  ssltd  27836  sssslt1  27840  sssslt2  27841  syl22anbrc  32474  fldgenfldext  33718  weiunso  36467  prjspertr  42615  prjspvs  42620  0prjspnrel  42637  nla0002  43437  nla0003  43438  clnbgrvtxel  47816  clnbgredg  47826