Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iscsgrpALT Structured version   Visualization version   Unicode version

Theorem iscsgrpALT 39915
 Description: The predicate "is a commutative semigroup." (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ismgmALT.b
ismgmALT.o
Assertion
Ref Expression
iscsgrpALT CSGrpALT SGrpALT comLaw

Proof of Theorem iscsgrpALT
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fveq2 5865 . . . 4
2 fveq2 5865 . . . 4
31, 2breq12d 4415 . . 3 comLaw comLaw
4 ismgmALT.o . . . 4
5 ismgmALT.b . . . 4
64, 5breq12i 4411 . . 3 comLaw comLaw
73, 6syl6bbr 267 . 2 comLaw comLaw
8 df-csgrp2 39911 . 2 CSGrpALT SGrpALT comLaw
97, 8elrab2 3198 1 CSGrpALT SGrpALT comLaw
 Colors of variables: wff setvar class Syntax hints:   wb 188   wa 371   wceq 1444   wcel 1887   class class class wbr 4402  cfv 5582  cbs 15121   cplusg 15190   comLaw ccomlaw 39874  SGrpALTcsgrp2 39906  CSGrpALTccsgrp2 39907 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-csgrp2 39911 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator