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

Theorem eqcoms 2445
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 2444 . 2  |-  ( B  =  A  <->  A  =  B )
2 eqcoms.1 . 2  |-  ( A  =  B  ->  ph )
31, 2sylbi 189 1  |-  ( B  =  A  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  gencbvex  3004  sbceq2a  3178  eqimss2  3387  uneqdifeq  3740  tppreq3  3933  tpprceq3  3962  copsex2t  4472  copsex2g  4473  tfindsg  4869  findsg  4901  cnveqb  5355  cnveq0  5356  relcoi1  5427  unixpid  5433  funtpg  5530  tz6.12i  5780  f1ocnvfv  6045  f1ocnvfvb  6046  cbvfo  6051  ov6g  6240  ectocld  7000  ecoptocl  7023  undifixp  7127  phplem3  7317  card1  7886  pr2ne  7920  prdom2  7921  sornom  8188  indpi  8815  ltlen  9206  eqlei  9214  squeeze0  9944  nn0ind-raph  10401  injresinjlem  11230  hashf1rn  11667  hash1snb  11712  hashgt12el  11713  hashgt12el2  11714  hash2prde  11719  brfi1uzind  11746  rennim  12075  absmod0  12139  xpsfrnel2  13821  istos  14495  odbezout  15225  frgpnabllem1  15515  bwth  17504  txcn  17689  qtopeu  17779  reeff1o  20394  pntrlog2bndlem5  21306  usgraedg4  21437  usgraidx2vlem2  21442  nbgraf1olem5  21486  nb3graprlem1  21491  cusgrasize2inds  21517  usgrasscusgra  21523  2pthlem2  21627  wlkdvspthlem  21638  fargshiftfv  21653  fargshiftf  21654  usgrcyclnl1  21658  usgrcyclnl2  21659  3v3e3cycl1  21662  constr3trllem2  21669  4cycl4v4e  21684  4cycl4dv4e  21686  vdusgra0nedg  21710  usgravd0nedg  21714  eupatrl  21721  ismgm  21939  rngodm1dm2  22037  rngomndo  22040  rngoueqz  22049  zerdivemp1  22053  cdj1i  23967  br8  25410  br4  25412  sspred  25478  mblfinlem3  26281  mblfinlem4  26282  itg2addnclem  26294  indexdom  26474  zerdivemp1x  26609  pm13.192  27625  iotavalsb  27648  nvelim  27992  fveqvfvv  28002  funressnfv  28006  afvpcfv0  28024  afv0nbfvbi  28029  fnbrafvb  28032  tz6.12-afv  28051  afvco2  28054  ndmaovg  28062  f0rn0  28117  oprabv  28127  fzoopth  28186  euhash1  28214  swrdccatin12lem3  28270  swrdccatin12lem4  28271  swrdccat3a  28275  swrdccatin1d  28278  lswrdn0  28318  cshweqdif2  28328  cshweqdif2s  28329  cshweqrep  28332  cshwsexa  28349  wlkn0  28356  usg2wlkeq  28366  usgra2wlkspthlem1  28368  usgra2pth  28373  wwlkn0  28395  wlkiswwlk1  28396  wlkiswwlk2lem3  28399  wlklniswwlkn1  28405  el2wlkonot  28425  el2spthonot  28426  el2spthonot0  28427  el2wlkonotot0  28428  el2wlkonotot1  28430  usg2spthonot0  28445  1to2vfriswmgra  28494  frgrancvvdeqlem3  28519  frgrancvvdeqlem4  28520  frgrancvvdeqlemB  28525  frgrancvvdeqlemC  28526  usgreghash2spotv  28553  opcon3b  30092  ps-1  30372  3atlem5  30382  4atex  30971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-cleq 2435
  Copyright terms: Public domain W3C validator