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

Theorem eqcomd 2145
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 2141 . 2  |-  ( A  =  B  <->  B  =  A )
31, 2sylib 121 1  |-  ( ph  ->  B  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  eqtr2d  2173  eqtr3d  2174  eqtr4d  2175  syl5req  2185  syl6req  2189  sylan9req  2193  eqeltrrd  2217  eleqtrrd  2219  eleqtrrid  2229  eqeltrrdi  2231  eqnetrrd  2334  neeqtrrd  2338  rspcedeq2vd  2799  dedhb  2853  eqsstrrd  3134  sseqtrrd  3136  eqsstrrdi  3150  dfrab3ss  3354  uneqdifeqim  3448  ifbothdadc  3503  ifbothdc  3504  disjsn2  3586  diftpsn3  3661  dfopg  3703  unimax  3770  sndisj  3925  eqbrtrrd  3952  breqtrrd  3956  breqtrrid  3966  eqbrtrrdi  3968  class2seteq  4087  opth1  4158  euotd  4176  opelopabsb  4182  tfisi  4501  0nelxp  4567  opeliunxp  4594  euiotaex  5104  iota4  5106  fun2ssres  5166  funimass1  5200  funssfv  5447  fnimapr  5481  fvun1  5487  fvco4  5493  elfvmptrab  5516  fmptco  5586  foima2  5653  foeqcnvco  5691  f1eqcocnv  5692  f1oiso2  5728  riotass2  5756  riotass  5757  f1ocnvfv3  5763  caovlem2d  5963  f1opw2  5976  sbcopeq1a  6085  csbopeq1a  6086  eloprabi  6094  cnvf1olem  6121  f2ndf  6123  smoiso  6199  nnaword  6407  eqer  6461  uniqs  6487  mapsncnv  6589  ixpiinm  6618  mapsnf1o  6631  ssenen  6745  findcard2  6783  findcard2s  6784  unsnfidcex  6808  fisseneq  6820  phpeqd  6821  en1eqsn  6836  sbthlemi6  6850  updjud  6967  omp1eomlem  6979  fodju0  7019  enq0sym  7247  enq0tr  7249  recexgt0sr  7588  caucvgsrlemoffcau  7613  axcaucvglemval  7712  le2tri3i  7879  cnegexlem2  7945  nnpcan  7992  addlsub  8139  negf1o  8151  subdi  8154  rereim  8355  cru  8371  divmulassap  8462  divmulasscomap  8463  divap1d  8568  div4p1lem1div2  8980  elz2  9129  zindd  9176  qapne  9438  divge1  9517  xrlttri3  9590  fseq1p1m1  9881  fzrevral  9892  nn0disj  9922  fzosplitsnm1  9993  fzosplitprm1  10018  flqlelt  10056  divfl0  10076  flqpmodeq  10107  zmodidfzo  10133  modqmuladd  10146  qnegmod  10149  addmodid  10152  modifeq2int  10166  modqeqmodmin  10174  modfzo0difsn  10175  modsumfzodifsn  10176  addmodlteq  10178  frecuzrdgsuc  10194  frecfzen2  10207  iseqf1olemab  10269  iseqf1olemmo  10272  ser3sub  10286  expgt1  10338  leexp2r  10354  sqoddm1div8  10451  bcm1k  10513  bcn2m1  10522  hashinfuni  10530  hashennnuni  10532  hashennn  10533  hashunlem  10557  hashprg  10561  fihashssdif  10571  zfz1isolem1  10590  shftlem  10595  shftfvalg  10597  shftfval  10600  replim  10638  cjexp  10672  resqrexlemcalc1  10793  resqrexlemcvg  10798  rersqrtthlem  10809  abssq  10860  recan  10888  negfi  11006  minclpr  11015  xrmaxiflemcom  11025  xrmineqinf  11045  xrminltinf  11048  xrminadd  11051  climmpt  11076  climrecl  11100  fsum3cvg  11154  summodclem3  11156  summodclem2a  11157  modfsummodlemstep  11233  isumsplit  11267  arisum  11274  geosergap  11282  geo2sum  11290  mertenslemi1  11311  mertenslem2  11312  clim2divap  11316  fproddccvg  11348  efcj  11386  efsub  11394  eflegeo  11414  sinneg  11439  cosneg  11440  sin01bnd  11470  cos01bnd  11471  summodnegmod  11530  dvdseq  11552  addmodlteqALT  11563  mulmoddvds  11567  zob  11594  nn0ob  11611  divalgmod  11630  flodddiv4  11637  divgcdnnr  11670  gcdneg  11676  bezoutlemsup  11703  dvdssq  11725  lcmneg  11761  3lcm2e6woprm  11773  6lcm4e12  11774  divgcdcoprmex  11789  cncongr1  11790  cncongrcoprm  11793  oddpwdclemxy  11853  oddpwdclemodd  11856  divnumden  11880  zgcdsq  11885  phibnd  11899  hashgcdlem  11909  ennnfonelemex  11933  strndxid  11996  topnvalg  12141  toponcom  12203  tgtopon  12244  restopnb  12359  cnptoprest  12417  blfvalps  12563  bdmopn  12682  cnmet  12708  limcdifap  12809  dviaddf  12847  dvexp  12853  coseq0negpitopi  12933  abssinper  12943  subctctexmid  13249  cvgcmp2nlemabs  13280  trilpolemlt1  13287
  Copyright terms: Public domain W3C validator