Theorem syl21anbrc 1346

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  8243  erinxp  8731  frrlem15  9672  fpwwe2lem11  10555  nqerf  10844  nqerid  10847  genpcl  10922  nqpr  10928  ltexprlem5  10954  psss  18537  psssdm2  18538  ismhmd  18745  idmhm  18754  resmhm2b  18781  prdspjmhm  18788  pwsdiagmhm  18790  pwsco1mhm  18791  pwsco2mhm  18792  frmdup1  18823  mhmfmhm  19032  isghmd  19191  ghmmhm  19192  idghm  19197  symgsubmefmndALT  19369  lactghmga  19371  frgpmhm  19731  frgpuplem  19738  mulgmhm  19793  isrhm2d  20457  idrhm  20460  pwsco1rhm  20470  pwsco2rhm  20471  subrgid  20541  issubrg2  20560  subsubrg  20566  pwsdiagrhm  20575  islmhmd  21026  reslmhm  21039  rngqiprngho  21293  issubassa  21857  subrgpsr  21966  mat1mhm  22459  mat1rhm  22460  scmatmhm  22509  scmatrhm  22510  mat2pmatmhm  22708  mat2pmatrhm  22709  m2cpmrhm  22721  pm2mpmhm  22795  pm2mprhm  22796  ptpjcn  23586  idnmhm  24729  pi1cpbl  25021  pi1grplem  25026  pi1xfr  25032  pi1coghm  25038  vitalilem1  25585  vitalilem3  25587  sltsd  27774  ssslts1  27779  ssslts2  27780  syl22anbrc  32540  fldgenfldext  33828  weiunso  36664  prjspertr  43052  prjspvs  43057  0prjspnrel  43074  nla0002  43869  nla0003  43870  clnbgrvtxel  48317  clnbgredg  48328