MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqcoms Unicode version

Theorem eqcoms 2286
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcoms.1  |-  ( A  =  B  ->  ph )
Assertion
Ref Expression
eqcoms  |-  ( B  =  A  ->  ph )

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2285 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 187 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  gencbvex  2830  sbceq2a  3002  sbcco2  3014  eqimss2  3231  uneqdifeq  3542  copsex2t  4253  copsex2g  4254  snnex  4524  tfisi  4649  tfindsg  4651  findsg  4683  opeliunxp  4740  elrnmpt1  4928  cnveqb  5129  cnveq0  5130  relcoi1  5201  unixpid  5207  iotaval  5230  tz6.12i  5548  elabrex  5765  opabex3  5769  f1ocnvfv  5794  f1ocnvfvb  5795  cbvfo  5799  ov6g  5985  ectocld  6726  ecoptocl  6748  undifixp  6852  phplem3  7042  ixpiunwdom  7305  card1  7601  pr2ne  7635  prdom2  7636  sornom  7903  indpi  8531  ltlen  8922  squeeze0  9659  nn0ind-raph  10112  rennim  11724  absmod0  11788  imasvscafn  13439  xpsfrnel2  13467  istos  14141  odbezout  14871  frgpnabllem1  15161  ptbasfi  17276  txcn  17320  qtopeu  17407  iundisj2  18906  reeff1o  19823  dchrisumlema  20637  dchrisumlem2  20639  pntrlog2bndlem5  20730  ismgm  20987  rngodm1dm2  21085  rngomndo  21088  rngoueqz  21097  cdj1i  23013  iundisj2fi  23364  iundisj2f  23366  br8  24113  br4  24115  sspred  24174  splint  25048  oooeqim2  25053  scprefat2  25072  injsurinj  25149  cbcpcp  25162  prl2  25169  islatalg  25183  jidd  25192  midd  25193  cur1vald  25199  int2pre  25237  posprsr  25240  dupre2  25244  sege  25252  ubos  25256  mxlmnl2  25270  defse3  25272  geme2  25275  supwval  25284  dfps2  25289  isdir2  25292  ridlideq  25335  rzrlzreq  25336  mgmlion  25337  grpodivfo  25374  imtr  25398  rngodmeqrn  25419  zerdivemp1  25436  svs2  25487  svs3  25488  unint2t  25518  intfmu2  25519  nsn  25530  intopcoaconlem3b  25538  intopcoaconlem3  25539  intcont  25543  islimrs3  25581  islimrs4  25582  bwt2  25592  supnuf  25629  addcanri  25666  addcanrg  25667  negveud  25668  negveudr  25669  tcnvec  25690  hdrmp  25706  ismona  25809  iepiclem  25823  isepic  25824  idfisf  25841  propsrc  25868  prismorcsetlemc  25917  cmpmor  25975  setiscat  25979  clscnc  26010  smbkle  26043  cndpv  26049  pgapspf  26052  lineval2a  26085  lineval6a  26089  sgplpte21d1  26139  lppotoslem  26143  xsyysx  26145  bsstrs  26146  nbssntrs  26147  isibcg  26191  indexdom  26413  fdc  26455  zerdivemp1x  26586  pm13.192  27610  iotavalsb  27633  rfcnnnub  27707  nvelim  27978  fveqvfvv  27987  funressnfv  27991  afvpcfv0  28009  afvvfveq  28011  afv0nbfvbi  28014  fnbrafvb  28016  tz6.12-afv  28035  afvco2  28037  ndmaovg  28044  tppreq3  28071  tpprceq3  28072  1to2vfriswmgra  28184  opcon3b  29386  ps-1  29666  3atlem5  29676  4atex  30265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator