Theorem syl21anbrc 1344

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  8341  erinxp  8849  frrlem15  9826  fpwwe2lem11  10710  nqerf  10999  nqerid  11002  genpcl  11077  nqpr  11083  ltexprlem5  11109  psss  18650  psssdm2  18651  ismhmd  18821  idmhm  18830  resmhm2b  18857  prdspjmhm  18864  pwsdiagmhm  18866  pwsco1mhm  18867  pwsco2mhm  18868  frmdup1  18899  mhmfmhm  19105  isghmd  19265  ghmmhm  19266  idghm  19271  symgsubmefmndALT  19445  lactghmga  19447  frgpmhm  19807  frgpuplem  19814  mulgmhm  19869  isrhm2d  20513  idrhm  20516  pwsco1rhm  20528  pwsco2rhm  20529  subrgid  20601  issubrg2  20620  subsubrg  20626  pwsdiagrhm  20635  islmhmd  21061  reslmhm  21074  rngqiprngho  21336  issubassa  21910  subrgpsr  22021  mat1mhm  22511  mat1rhm  22512  scmatmhm  22561  scmatrhm  22562  mat2pmatmhm  22760  mat2pmatrhm  22761  m2cpmrhm  22773  pm2mpmhm  22847  pm2mprhm  22848  ptpjcn  23640  idnmhm  24796  pi1cpbl  25096  pi1grplem  25101  pi1xfr  25107  pi1coghm  25113  vitalilem1  25662  vitalilem3  25664  ssltd  27854  sssslt1  27858  sssslt2  27859  fldgenfldext  33678  weiunso  36432  prjspertr  42560  prjspvs  42565  0prjspnrel  42582  nla0002  43386  nla0003  43387  clnbgrvtxel  47702  clnbgredg  47712