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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fprlem1  8030  erinxp  8462  fpwwe2lem11  10238  nqerf  10527  nqerid  10530  genpcl  10605  nqpr  10611  ltexprlem5  10637  psss  18058  psssdm2  18059  idmhm  18199  resmhm2b  18221  prdspjmhm  18227  pwsdiagmhm  18229  pwsco1mhm  18230  pwsco2mhm  18231  frmdup1  18263  mhmfmhm  18458  isghmd  18603  ghmmhm  18604  idghm  18609  symgsubmefmndALT  18767  lactghmga  18769  frgpmhm  19127  frgpuplem  19134  mulgmhm  19185  isrhm2d  19720  idrhm  19723  pwsco1rhm  19730  pwsco2rhm  19731  subrgid  19774  issubrg2  19792  subsubrg  19798  pwsdiagrhm  19806  islmhmd  20048  reslmhm  20061  issubassa  20800  subrgpsr  20916  mat1mhm  21353  mat1rhm  21354  scmatmhm  21403  scmatrhm  21404  mat2pmatmhm  21602  mat2pmatrhm  21603  m2cpmrhm  21615  pm2mpmhm  21689  pm2mprhm  21690  ptpjcn  22480  idnmhm  23624  pi1cpbl  23913  pi1grplem  23918  pi1xfr  23924  pi1coghm  23930  vitalilem1  24477  vitalilem3  24479  frrlem15  33513  ssltd  33680  sssslt1  33683  sssslt2  33684  ismhmd  39903  prjspertr  40104  prjspvs  40109  0prjspnrel  40124