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

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
StepHypRef Expression
1 syl21anbrc.1 . . 3 (𝜑𝜓)
2 syl21anbrc.2 . . 3 (𝜑𝜒)
3 syl21anbrc.3 . . 3 (𝜑𝜃)
41, 2, 3jca31 515 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 syl21anbrc.4 . 2 (𝜏 ↔ ((𝜓𝜒) ∧ 𝜃))
64, 5sylibr 233 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 206  df-an 397
This theorem is referenced by:  fprlem1  8223  erinxp  8688  frrlem15  9651  fpwwe2lem11  10535  nqerf  10824  nqerid  10827  genpcl  10902  nqpr  10908  ltexprlem5  10934  psss  18429  psssdm2  18430  ismhmd  18564  idmhm  18571  resmhm2b  18593  prdspjmhm  18599  pwsdiagmhm  18601  pwsco1mhm  18602  pwsco2mhm  18603  frmdup1  18634  mhmfmhm  18829  isghmd  18976  ghmmhm  18977  idghm  18982  symgsubmefmndALT  19144  lactghmga  19146  frgpmhm  19506  frgpuplem  19513  mulgmhm  19565  isrhm2d  20113  idrhm  20116  pwsco1rhm  20125  pwsco2rhm  20126  subrgid  20177  issubrg2  20195  subsubrg  20201  pwsdiagrhm  20209  islmhmd  20453  reslmhm  20466  issubassa  21225  subrgpsr  21340  mat1mhm  21785  mat1rhm  21786  scmatmhm  21835  scmatrhm  21836  mat2pmatmhm  22034  mat2pmatrhm  22035  m2cpmrhm  22047  pm2mpmhm  22121  pm2mprhm  22122  ptpjcn  22914  idnmhm  24070  pi1cpbl  24359  pi1grplem  24364  pi1xfr  24370  pi1coghm  24376  vitalilem1  24924  vitalilem3  24926  ssltd  27083  sssslt1  27086  sssslt2  27087  prjspertr  40852  prjspvs  40857  0prjspnrel  40874  nla0002  41607  nla0003  41608
  Copyright terms: Public domain W3C validator