ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqcomd Unicode version

Theorem eqcomd 2087
Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
eqcomd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eqcomd  |-  ( ph  ->  B  =  A )

Proof of Theorem eqcomd
StepHypRef Expression
1 eqcomd.1 . 2  |-  ( ph  ->  A  =  B )
2 eqcom 2084 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 120 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqtr2d  2115  eqtr3d  2116  eqtr4d  2117  syl5req  2127  syl6req  2131  sylan9req  2135  eqeltrrd  2157  eleqtrrd  2159  syl5eleqr  2169  syl6eqelr  2171  eqnetrrd  2272  neeqtrrd  2276  rspcedeq2vd  2711  dedhb  2762  eqsstr3d  3035  sseqtr4d  3037  syl6eqssr  3051  dfrab3ss  3249  uneqdifeqim  3335  ifbothdc  3388  disjsn2  3463  diftpsn3  3535  dfopg  3576  unimax  3643  sndisj  3789  eqbrtrrd  3815  breqtrrd  3819  syl5breqr  3829  syl6eqbrr  3831  class2seteq  3945  opth1  3999  euotd  4017  opelopabsb  4023  tfisi  4336  0nelxp  4398  opeliunxp  4421  euiotaex  4913  iota4  4915  fun2ssres  4973  funimass1  5007  funssfv  5231  fnimapr  5265  fvun1  5271  fmptco  5362  foeqcnvco  5461  f1eqcocnv  5462  f1oiso2  5497  riotass2  5525  riotass  5526  f1ocnvfv3  5532  caovlem2d  5724  f1opw2  5737  sbcopeq1a  5844  csbopeq1a  5845  eloprabi  5853  cnvf1olem  5876  f2ndf  5878  smoiso  5951  nnaword  6150  eqer  6204  uniqs  6230  findcard2  6423  findcard2s  6424  unsnfidcex  6440  enq0sym  6684  enq0tr  6686  recexgt0sr  7012  caucvgsrlemoffcau  7036  axcaucvglemval  7125  le2tri3i  7286  cnegexlem2  7351  nnpcan  7398  addlsub  7541  negf1o  7553  subdi  7556  rereim  7753  cru  7769  divmulassap  7850  divmulasscomap  7851  divap1d  7955  div4p1lem1div2  8351  elz2  8500  zindd  8546  qapne  8805  divge1  8881  xrlttri3  8948  fseq1p1m1  9187  fzrevral  9198  nn0disj  9225  fzosplitsnm1  9295  fzosplitprm1  9320  flqlelt  9358  divfl0  9378  flqpmodeq  9409  zmodidfzo  9435  modqmuladd  9448  qnegmod  9451  addmodid  9454  modifeq2int  9468  modqeqmodmin  9476  modfzo0difsn  9477  modsumfzodifsn  9478  addmodlteq  9480  frecuzrdgsuc  9496  frecfzen2  9509  isersub  9560  expgt1  9611  leexp2r  9627  sqoddm1div8  9722  bcm1k  9784  bcn2m1  9793  sizeinfuni  9801  sizeennnuni  9803  sizeennn  9804  sizeunlem  9828  sizeprg  9832  shftlem  9842  shftfvalg  9844  shftfval  9847  replim  9884  cjexp  9918  resqrexlemcalc1  10038  resqrexlemcvg  10043  rersqrtthlem  10054  abssq  10105  recan  10133  negfi  10248  climmpt  10277  climrecl  10300  fisumcvg  10338  summodnegmod  10371  dvdseq  10393  addmodlteqALT  10404  mulmoddvds  10408  zob  10435  nn0ob  10452  divalgmod  10471  flodddiv4  10478  divgcdnnr  10511  gcdneg  10517  bezoutlemsup  10542  dvdssq  10564  lcmneg  10600  3lcm2e6woprm  10612  6lcm4e12  10613  divgcdcoprmex  10628  cncongr1  10629  cncongrcoprm  10632  oddpwdclemxy  10691  oddpwdclemodd  10694
  Copyright terms: Public domain W3C validator