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

Theorem eqcoms 2438
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 2437 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 188 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  gencbvex  2990  sbceq2a  3164  eqimss2  3393  uneqdifeq  3708  tppreq3  3901  tpprceq3  3930  copsex2t  4435  copsex2g  4436  tfindsg  4831  findsg  4863  cnveqb  5317  cnveq0  5318  relcoi1  5389  unixpid  5395  funtpg  5492  tz6.12i  5742  f1ocnvfv  6007  f1ocnvfvb  6008  cbvfo  6013  ov6g  6202  ectocld  6962  ecoptocl  6985  undifixp  7089  phplem3  7279  card1  7844  pr2ne  7878  prdom2  7879  sornom  8146  indpi  8773  ltlen  9164  eqlei  9172  squeeze0  9902  nn0ind-raph  10359  injresinjlem  11187  hashf1rn  11624  hash1snb  11669  hashgt12el  11670  hashgt12el2  11671  hash2prde  11676  brfi1uzind  11703  rennim  12032  absmod0  12096  xpsfrnel2  13778  istos  14452  odbezout  15182  frgpnabllem1  15472  bwth  17461  txcn  17646  qtopeu  17736  reeff1o  20351  pntrlog2bndlem5  21263  usgraedg4  21394  usgraidx2vlem2  21399  nbgraf1olem5  21443  nb3graprlem1  21448  cusgrasize2inds  21474  usgrasscusgra  21480  2pthlem2  21584  wlkdvspthlem  21595  fargshiftfv  21610  fargshiftf  21611  usgrcyclnl1  21615  usgrcyclnl2  21616  3v3e3cycl1  21619  constr3trllem2  21626  4cycl4v4e  21641  4cycl4dv4e  21643  vdusgra0nedg  21667  usgravd0nedg  21671  eupatrl  21678  ismgm  21896  rngodm1dm2  21994  rngomndo  21997  rngoueqz  22006  zerdivemp1  22010  cdj1i  23924  br8  25368  br4  25370  sspred  25429  mblfinlem2  26191  mblfinlem3  26192  itg2addnclem  26202  indexdom  26373  zerdivemp1x  26508  pm13.192  27525  iotavalsb  27548  nvelim  27892  fveqvfvv  27902  funressnfv  27906  afvpcfv0  27924  afv0nbfvbi  27929  fnbrafvb  27932  tz6.12-afv  27951  afvco2  27954  ndmaovg  27962  euhash1  28071  swrdccatin2  28093  swrdccatin12lem3  28099  swrdccatin12lem4  28100  swrdccatin12  28101  swrdccatin12b  28102  swrdccat3  28104  swrdccat3a  28105  lswrdn0  28149  shwrdeqdif2  28156  shwrdeqdif2s  28157  shwrdeqrep  28160  usgra2wlkspthlem1  28180  usgra2pth  28185  el2wlkonot  28210  el2spthonot  28211  el2spthonot0  28212  el2wlkonotot0  28213  el2wlkonotot1  28215  usg2spthonot0  28230  1to2vfriswmgra  28254  frgrancvvdeqlem3  28279  frgrancvvdeqlem4  28280  frgrancvvdeqlemB  28285  frgrancvvdeqlemC  28286  usgreghash2spotv  28313  opcon3b  29833  ps-1  30113  3atlem5  30123  4atex  30712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428
  Copyright terms: Public domain W3C validator