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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  fprlem1  8285  erinxp  8785  frrlem15  9752  fpwwe2lem11  10636  nqerf  10925  nqerid  10928  genpcl  11003  nqpr  11009  ltexprlem5  11035  psss  18533  psssdm2  18534  ismhmd  18674  idmhm  18681  resmhm2b  18703  prdspjmhm  18710  pwsdiagmhm  18712  pwsco1mhm  18713  pwsco2mhm  18714  frmdup1  18745  mhmfmhm  18948  isghmd  19101  ghmmhm  19102  idghm  19107  symgsubmefmndALT  19271  lactghmga  19273  frgpmhm  19633  frgpuplem  19640  mulgmhm  19695  isrhm2d  20265  idrhm  20268  pwsco1rhm  20277  pwsco2rhm  20278  subrgid  20321  issubrg2  20339  subsubrg  20345  pwsdiagrhm  20354  islmhmd  20650  reslmhm  20663  issubassa  21421  subrgpsr  21539  mat1mhm  21986  mat1rhm  21987  scmatmhm  22036  scmatrhm  22037  mat2pmatmhm  22235  mat2pmatrhm  22236  m2cpmrhm  22248  pm2mpmhm  22322  pm2mprhm  22323  ptpjcn  23115  idnmhm  24271  pi1cpbl  24560  pi1grplem  24565  pi1xfr  24571  pi1coghm  24577  vitalilem1  25125  vitalilem3  25127  ssltd  27293  sssslt1  27296  sssslt2  27297  prjspertr  41347  prjspvs  41352  0prjspnrel  41369  nla0002  42175  nla0003  42176  rngqiprngho  46788