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

Theorem eqcoms 2299
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 2298 . 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 1632
This theorem is referenced by:  gencbvex  2843  sbceq2a  3015  sbcco2  3027  eqimss2  3244  uneqdifeq  3555  copsex2t  4269  copsex2g  4270  snnex  4540  tfisi  4665  tfindsg  4667  findsg  4699  opeliunxp  4756  elrnmpt1  4944  cnveqb  5145  cnveq0  5146  relcoi1  5217  unixpid  5223  iotaval  5246  tz6.12i  5564  elabrex  5781  opabex3  5785  f1ocnvfv  5810  f1ocnvfvb  5811  cbvfo  5815  ov6g  6001  ectocld  6742  ecoptocl  6764  undifixp  6868  phplem3  7058  ixpiunwdom  7321  card1  7617  pr2ne  7651  prdom2  7652  sornom  7919  indpi  8547  ltlen  8938  squeeze0  9675  nn0ind-raph  10128  rennim  11740  absmod0  11804  imasvscafn  13455  xpsfrnel2  13483  istos  14157  odbezout  14887  frgpnabllem1  15177  ptbasfi  17292  txcn  17336  qtopeu  17423  iundisj2  18922  reeff1o  19839  dchrisumlema  20653  dchrisumlem2  20655  pntrlog2bndlem5  20746  ismgm  21003  rngodm1dm2  21101  rngomndo  21104  rngoueqz  21113  cdj1i  23029  iundisj2fi  23379  iundisj2f  23381  br8  24184  br4  24186  sspred  24245  splint  25151  oooeqim2  25156  scprefat2  25175  injsurinj  25252  cbcpcp  25265  prl2  25272  islatalg  25286  jidd  25295  midd  25296  cur1vald  25302  int2pre  25340  posprsr  25343  dupre2  25347  sege  25355  ubos  25359  mxlmnl2  25373  defse3  25375  geme2  25378  supwval  25387  dfps2  25392  isdir2  25395  ridlideq  25438  rzrlzreq  25439  mgmlion  25440  grpodivfo  25477  imtr  25501  rngodmeqrn  25522  zerdivemp1  25539  svs2  25590  svs3  25591  unint2t  25621  intfmu2  25622  nsn  25633  intopcoaconlem3b  25641  intopcoaconlem3  25642  intcont  25646  islimrs3  25684  islimrs4  25685  bwt2  25695  supnuf  25732  addcanri  25769  addcanrg  25770  negveud  25771  negveudr  25772  tcnvec  25793  hdrmp  25809  ismona  25912  iepiclem  25926  isepic  25927  idfisf  25944  propsrc  25971  prismorcsetlemc  26020  cmpmor  26078  setiscat  26082  clscnc  26113  smbkle  26146  cndpv  26152  pgapspf  26155  lineval2a  26188  lineval6a  26192  sgplpte21d1  26242  lppotoslem  26246  xsyysx  26248  bsstrs  26249  nbssntrs  26250  isibcg  26294  indexdom  26516  fdc  26558  zerdivemp1x  26689  pm13.192  27713  iotavalsb  27736  rfcnnnub  27810  nvelim  28081  fveqvfvv  28092  funressnfv  28096  afvpcfv0  28114  afvvfveq  28116  afv0nbfvbi  28119  fnbrafvb  28122  tz6.12-afv  28141  afvco2  28144  ndmaovg  28152  tppreq3  28181  tpprceq3  28182  injresinjlem  28214  hashgt12el  28218  hashgt12el2  28219  nb3graprlem1  28287  wlkdvspthlem  28365  fargshiftfv  28380  fargshiftf  28381  eupatrl  28385  usgrcyclnl1  28386  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3trllem2  28397  4cycl4v4e  28412  4cycl4dv4e  28414  1to2vfriswmgra  28430  opcon3b  30008  ps-1  30288  3atlem5  30298  4atex  30887
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator