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

Theorem eqcomd 2061
Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
eqcomd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eqcomd (𝜑𝐵 = 𝐴)

Proof of Theorem eqcomd
StepHypRef Expression
1 eqcomd.1 . 2 (𝜑𝐴 = 𝐵)
2 eqcom 2058 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
31, 2sylib 131 1 (𝜑𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtr2d  2089  eqtr3d  2090  eqtr4d  2091  syl5req  2101  syl6req  2105  sylan9req  2109  eqeltrrd  2131  eleqtrrd  2133  syl5eleqr  2143  syl6eqelr  2145  eqnetrrd  2246  neeqtrrd  2250  rspcedeq2vd  2682  dedhb  2732  eqsstr3d  3007  sseqtr4d  3009  syl6eqssr  3023  dfrab3ss  3242  uneqdifeqim  3335  ifbothdc  3384  disjsn2  3460  diftpsn3  3532  dfopg  3574  unimax  3641  sndisj  3787  eqbrtrrd  3813  breqtrrd  3817  syl5breqr  3827  syl6eqbrr  3829  class2seteq  3943  opth1  4000  euotd  4018  opelopabsb  4024  tfisi  4337  0nelxp  4399  opeliunxp  4422  euiotaex  4910  iota4  4912  fun2ssres  4970  funimass1  5003  funssfv  5226  fnimapr  5260  fvun1  5266  fmptco  5357  foeqcnvco  5457  f1eqcocnv  5458  f1oiso2  5493  riotass2  5521  riotass  5522  f1ocnvfv3  5528  caovlem2d  5720  f1opw2  5733  sbcopeq1a  5840  csbopeq1a  5841  eloprabi  5849  cnvf1olem  5872  f2ndf  5874  smoiso  5947  nnaword  6114  eqer  6168  uniqs  6194  findcard2  6376  findcard2s  6377  enq0sym  6587  enq0tr  6589  recexgt0sr  6915  caucvgsrlemoffcau  6939  axcaucvglemval  7028  le2tri3i  7184  cnegexlem2  7249  nnpcan  7296  addlsub  7439  subdi  7453  rereim  7650  cru  7666  divap1d  7850  div4p1lem1div2  8234  elz2  8369  zindd  8414  qapne  8670  divge1  8746  xrlttri3  8818  fseq1p1m1  9057  fzrevral  9068  nn0disj  9096  fzosplitsnm1  9166  fzosplitprm1  9191  flqlelt  9225  divfl0  9245  flqpmodeq  9276  zmodidfzo  9302  modqmuladd  9315  qnegmod  9318  addmodid  9321  modifeq2int  9335  modqeqmodmin  9343  modfzo0difsn  9344  modsumfzodifsn  9345  addmodlteq  9347  frecuzrdgsuc  9364  frecfzen2  9367  isersub  9407  expgt1  9457  leexp2r  9473  sqoddm1div8  9568  bcm1k  9627  bcn2m1  9636  shftlem  9644  shftfvalg  9646  shftfval  9649  replim  9686  cjexp  9720  resqrexlemcalc1  9840  resqrexlemcvg  9845  rersqrtthlem  9856  abssq  9907  recan  9935  climmpt  10051  climrecl  10074  summodnegmod  10137  dvdseq  10159  addmodlteqALT  10170  mulmoddvds  10174  zob  10202  nn0ob  10219  oddpwdclemxy  10236  oddpwdclemodd  10239
  Copyright terms: Public domain W3C validator