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

Theorem eqcoms 2439
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 2438 . 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  2998  sbceq2a  3172  eqimss2  3401  uneqdifeq  3716  tppreq3  3909  tpprceq3  3938  copsex2t  4443  copsex2g  4444  tfindsg  4840  findsg  4872  cnveqb  5326  cnveq0  5327  relcoi1  5398  unixpid  5404  funtpg  5501  tz6.12i  5751  f1ocnvfv  6016  f1ocnvfvb  6017  cbvfo  6022  ov6g  6211  ectocld  6971  ecoptocl  6994  undifixp  7098  phplem3  7288  card1  7855  pr2ne  7889  prdom2  7890  sornom  8157  indpi  8784  ltlen  9175  eqlei  9183  squeeze0  9913  nn0ind-raph  10370  injresinjlem  11199  hashf1rn  11636  hash1snb  11681  hashgt12el  11682  hashgt12el2  11683  hash2prde  11688  brfi1uzind  11715  rennim  12044  absmod0  12108  xpsfrnel2  13790  istos  14464  odbezout  15194  frgpnabllem1  15484  bwth  17473  txcn  17658  qtopeu  17748  reeff1o  20363  pntrlog2bndlem5  21275  usgraedg4  21406  usgraidx2vlem2  21411  nbgraf1olem5  21455  nb3graprlem1  21460  cusgrasize2inds  21486  usgrasscusgra  21492  2pthlem2  21596  wlkdvspthlem  21607  fargshiftfv  21622  fargshiftf  21623  usgrcyclnl1  21627  usgrcyclnl2  21628  3v3e3cycl1  21631  constr3trllem2  21638  4cycl4v4e  21653  4cycl4dv4e  21655  vdusgra0nedg  21679  usgravd0nedg  21683  eupatrl  21690  ismgm  21908  rngodm1dm2  22006  rngomndo  22009  rngoueqz  22018  zerdivemp1  22022  cdj1i  23936  br8  25379  br4  25381  sspred  25447  mblfinlem3  26245  mblfinlem4  26246  itg2addnclem  26256  indexdom  26436  zerdivemp1x  26571  pm13.192  27587  iotavalsb  27610  nvelim  27954  fveqvfvv  27964  funressnfv  27968  afvpcfv0  27986  afv0nbfvbi  27991  fnbrafvb  27994  tz6.12-afv  28013  afvco2  28016  ndmaovg  28024  oprabv  28085  fzoopth  28139  euhash1  28167  swrdccatin12lem3  28212  swrdccatin12lem4  28213  swrdccat3a  28217  swrdccatin1d  28220  lswrdn0  28260  cshweqdif2  28270  cshweqdif2s  28271  cshweqrep  28274  cshwsexa  28291  usg2wlkeq  28304  usgra2wlkspthlem1  28306  usgra2pth  28311  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  el2wlkonotot0  28339  el2wlkonotot1  28341  usg2spthonot0  28356  1to2vfriswmgra  28396  frgrancvvdeqlem3  28421  frgrancvvdeqlem4  28422  frgrancvvdeqlemB  28427  frgrancvvdeqlemC  28428  usgreghash2spotv  28455  opcon3b  29994  ps-1  30274  3atlem5  30284  4atex  30873
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 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429
  Copyright terms: Public domain W3C validator