MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl21anbrc Structured version   Visualization version   GIF version

Theorem syl21anbrc 1341
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
StepHypRef Expression
1 syl21anbrc.1 . . 3 (𝜑𝜓)
2 syl21anbrc.2 . . 3 (𝜑𝜒)
3 syl21anbrc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 518 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anbrc.4 . 2 (𝜏 ↔ ((𝜓𝜒) ∧ 𝜃))
64, 5sylibr 237 1 (𝜑𝜏)
Colors of variables: wff setvar class
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:  erinxp  8358  fpwwe2lem12  10056  nqerf  10345  nqerid  10348  genpcl  10423  nqpr  10429  ltexprlem5  10455  psss  17819  psssdm2  17820  idmhm  17960  resmhm2b  17982  prdspjmhm  17988  pwsdiagmhm  17990  pwsco1mhm  17991  pwsco2mhm  17992  frmdup1  18024  mhmfmhm  18217  isghmd  18362  ghmmhm  18363  idghm  18368  symgsubmefmndALT  18526  lactghmga  18528  frgpmhm  18886  frgpuplem  18893  mulgmhm  18944  isrhm2d  19479  idrhm  19482  pwsco1rhm  19489  pwsco2rhm  19490  subrgid  19533  issubrg2  19551  subsubrg  19557  pwsdiagrhm  19565  islmhmd  19807  reslmhm  19820  issubassa  20558  subrgpsr  20660  mat1mhm  21092  mat1rhm  21093  scmatmhm  21142  scmatrhm  21143  mat2pmatmhm  21341  mat2pmatrhm  21342  m2cpmrhm  21354  pm2mpmhm  21428  pm2mprhm  21429  ptpjcn  22219  idnmhm  23363  pi1cpbl  23652  pi1grplem  23657  pi1xfr  23663  pi1coghm  23669  vitalilem1  24215  vitalilem3  24217  fprlem1  33245  frrlem15  33250  sssslt1  33368  sssslt2  33369  prjspertr  39586  prjspvs  39591  0prjspnrel  39600
  Copyright terms: Public domain W3C validator