Theorem syl21anbrc 1325

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  erinxp  8169  fpwwe2lem12  9859  nqerf  10148  nqerid  10151  genpcl  10226  nqpr  10232  ltexprlem5  10258  psss  17694  psssdm2  17695  idmhm  17824  resmhm2b  17841  prdspjmhm  17847  pwsdiagmhm  17849  pwsco1mhm  17850  pwsco2mhm  17851  frmdup1  17882  mhmfmhm  18021  isghmd  18150  ghmmhm  18151  idghm  18156  lactghmga  18305  frgpmhm  18663  frgpuplem  18670  mulgmhm  18718  isrhm2d  19215  idrhm  19218  pwsco1rhm  19225  pwsco2rhm  19226  subrgid  19272  issubrg2  19290  subsubrg  19296  pwsdiagrhm  19303  islmhmd  19545  reslmhm  19558  issubassa  19830  subrgpsr  19925  mat1mhm  20812  mat1rhm  20813  scmatmhm  20862  scmatrhm  20863  mat2pmatmhm  21060  mat2pmatrhm  21061  m2cpmrhm  21073  pm2mpmhm  21147  pm2mprhm  21148  ptpjcn  21938  idnmhm  23081  pi1cpbl  23366  pi1grplem  23371  pi1xfr  23377  pi1coghm  23383  vitalilem1  23927  vitalilem3  23929  fprlem1  32695  frrlem15  32700  sssslt1  32818  sssslt2  32819  prjspertr  38700  prjspvs  38705  0prjspnrel  38714