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

Theorem eqtrd 2198
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrd.1 (𝜑𝐴 = 𝐵)
eqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtrd (𝜑𝐴 = 𝐶)

Proof of Theorem eqtrd
StepHypRef Expression
1 eqtrd.1 . 2 (𝜑𝐴 = 𝐵)
2 eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eqeq2d 2177 . 2 (𝜑 → (𝐴 = 𝐵𝐴 = 𝐶))
41, 3mpbid 146 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1343
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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-cleq 2158
This theorem is referenced by:  eqtr2d  2199  eqtr3d  2200  eqtr4d  2201  3eqtrd  2202  3eqtrrd  2203  3eqtr2d  2204  eqtrid  2210  syl5eq  2211  eqtrdi  2215  rabeqbidv  2721  rabeqbidva  2722  csbidmg  3101  csbco3g  3103  difeq12d  3241  ifeq12d  3539  ifbieq1d  3542  ifbieq2d  3544  ifbieq12d  3546  eqifdc  3554  csbsng  3637  disjpr2  3640  csbunig  3797  iuneq12d  3890  unisn3  4423  op1stbg  4457  opthreg  4533  onsucuni2  4541  csbxpg  4685  coeq12d  4768  csbdmg  4798  reseq12d  4885  csbresg  4887  resima2  4918  imaeq12d  4947  csbrng  5065  opswapg  5090  relcnvtr  5123  relcoi2  5134  relcoi1  5135  iotaint  5166  funprg  5238  funtpg  5239  funcnvres2  5263  fnco  5296  fococnv2  5458  fveq12d  5493  csbfv12g  5522  csbfv2g  5523  csbfvg  5524  dffn5im  5532  funfvdm2  5550  fvun1  5552  fvmpt2d  5572  fvmptt  5577  fndmin  5592  fniniseg2  5607  fnniniseg2  5608  fmptcof  5652  fvresi  5678  fvunsng  5679  fvpr1g  5691  fvpr2g  5692  fvtp1g  5693  funiunfvdm  5731  fcof1o  5757  riotaeqbidv  5801  oveq123d  5863  csbov12g  5881  csbov1g  5882  csbov2g  5883  ovmpodxf  5967  caov42d  6028  caovdilemd  6033  caovimo  6035  offeq  6063  offval2  6065  caofinvl  6072  ot1stg  6120  ot2ndg  6121  2nd1st  6148  mpomptsx  6165  dmmpossx  6167  fmpox  6168  fmpoco  6184  1stconst  6189  algrflemg  6198  tfrexlem  6302  rdgivallem  6349  rdgisuc1  6352  frec0g  6365  frecabcl  6367  frecsuclem  6374  frecrdg  6376  oa0  6425  oasuc  6432  oa1suc  6435  omsuc  6440  nnaass  6453  nndi  6454  nnmass  6455  nnm2  6493  nn2m  6494  ereq1  6508  errn  6523  uniqs2  6561  oviec  6607  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  mapsnconst  6660  mapen  6812  mapxpen  6814  xpmapenlem  6815  phplem4on  6833  fidifsnen  6836  undifdc  6889  fiintim  6894  fisseneq  6897  snexxph  6915  sbthlemi4  6925  sbthlemi6  6927  supeq2  6954  eqsupti  6961  infvalti  6987  djuf1olem  7018  djuss  7035  1stinl  7039  2ndinl  7040  1stinr  7041  2ndinr  7042  updjudhcoinlf  7045  updjudhcoinrg  7046  omp1eomlem  7059  difinfsn  7065  ctmlemr  7073  ctssdclemn0  7075  ctssdc  7078  enumctlemm  7079  nnnninfeq  7092  nnnninfeq2  7093  nninfisollemne  7095  nninfisol  7097  enwomnilem  7133  en2other2  7152  cc3  7209  mulidpi  7259  addasspig  7271  mulasspig  7273  distrpig  7274  indpi  7283  addcmpblnq  7308  mulpipq  7313  dmaddpqlem  7318  nqpi  7319  addcomnqg  7322  recrecnq  7335  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltaddnq  7348  ltexnqq  7349  archnqq  7358  prarloclemarch  7359  ltrnqg  7361  ltnnnq  7364  nq0nn  7383  addcmpblnq0  7384  nqpnq0nq  7394  nqnq0a  7395  nq0m0r  7397  nq0a0  7398  distrnq0  7400  addassnq0  7403  nq02m  7406  prarloclemlo  7435  prarloclemcalc  7443  addnqprllem  7468  addnqprulem  7469  addnqprl  7470  addnqpru  7471  appdivnq  7504  mulnqprl  7509  mulnqpru  7510  addcanprlemu  7556  ltaprlem  7559  ltmprr  7583  cauappcvgprlemladdrl  7598  mulcmpblnrlemg  7681  mulcomsrg  7698  distrsrg  7700  ltsosr  7705  1idsr  7709  00sr  7710  ltasrg  7711  recexgt0sr  7714  srpospr  7724  prsradd  7727  prsrriota  7729  caucvgsrlemcau  7734  caucvgsrlemgt1  7736  caucvgsrlemoffval  7737  caucvgsrlemoffres  7741  caucvgsr  7743  map2psrprg  7746  elreal2  7771  mulresr  7779  pitonnlem1p1  7787  pitonnlem2  7788  pitoregt0  7790  recidpirqlemcalc  7798  recidpirq  7799  axaddcl  7805  axmulcl  7807  axmulcom  7812  axmulass  7814  axdistr  7815  ax1rid  7818  axcnre  7822  recriota  7831  axcaucvglemcau  7839  mulid1  7896  mulid2  7897  adddirp1d  7925  joinlmuladdmuld  7926  muladd11  8031  1p1times  8032  readdcan  8038  comraddd  8055  add42  8060  npcan  8107  addsubass  8108  2addsub  8112  addsubeq4  8113  nppcan  8120  nnpcan  8121  npncan2  8125  nncan  8127  subsub  8128  nnncan  8133  nnncan1  8134  pnpcan2  8138  pnncan  8139  subneg  8147  negneg  8148  negdi2  8156  mvrraddd  8264  assraddsubd  8266  subaddeqd  8267  addid0  8271  mul02  8285  mul01  8287  mulneg1  8293  mul2neg  8296  mulm1  8298  ltadd2  8317  rimul  8483  rereim  8484  mulreim  8502  recextlem1  8548  mulcanapd  8558  divcanap1  8577  divrecap2  8585  divmulassap  8591  divmulasscomap  8592  divcanap4  8595  dividap  8597  muldivdirap  8603  divdivdivap  8609  recdivap  8614  divadddivap  8623  divsubdivap  8624  div2negap  8631  divcanap5rd  8714  dmdcanap2d  8717  subrecap  8735  recgt0  8745  lt2mul2div  8774  nnmulcl  8878  times2  8986  add1p1  9106  sub1m1  9107  cnm2m1cnm3  9108  nn0supp  9166  peano2z  9227  nneoor  9293  supminfex  9535  cnref1o  9588  rexneg  9766  xaddpnf1  9782  xaddmnf1  9784  rexadd  9788  xaddid1  9798  xaddid2  9799  xaddass  9805  xpncan  9807  xleadd1a  9809  xltadd1  9812  xposdif  9818  xadd4d  9821  xleaddadd  9823  iooidg  9845  iooval2  9851  icoshftf1o  9927  lincmb01cmp  9939  iccf1o  9940  fzval2  9947  fzsuc  10004  fzpred  10005  fztpval  10018  fseq1p1m1  10029  fzshftral  10043  fz0to4untppr  10059  fzo0to3tp  10154  fzo0sn0fzo1  10156  fzosplitsn  10168  fzosplitprm1  10169  fzisfzounsn  10171  rebtwn2zlemstep  10188  2tnp1ge0ge0  10236  flqdiv  10256  modqvalr  10260  modqdiffl  10270  modqfrac  10272  modqmulnn  10277  modqid  10284  modqcyc  10294  modqcyc2  10295  mulp1mod1  10300  modqmuladd  10301  modqmuladdnn0  10303  qnegmod  10304  m1modnnsub1  10305  addmodid  10307  addmodidr  10308  modqmul12d  10313  modqnegd  10314  modqadd12d  10315  modifeq2int  10321  modqaddmulmod  10326  modqdi  10327  modqsubdir  10328  modsumfzodifsn  10331  addmodlteq  10333  frec2uzsucd  10336  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdglem  10346  frecuzrdgsuc  10349  frecuzrdgg  10351  frecuzrdgdomlem  10352  frecuzrdgfunlem  10354  frecuzrdgtclt  10356  frecuzrdgsuctlem  10358  frecfzennn  10361  seqeq1  10383  seq3val  10393  seqvalcd  10394  seq3p1  10397  seqp1cd  10401  seq3feq2  10405  seq3fveq  10406  seq3shft2  10408  seq3-1p  10415  iseqf1olemnab  10423  iseqf1olemab  10424  iseqf1olemnanb  10425  iseqf1olemqk  10429  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1o  10439  seq3id3  10442  seq3z  10446  fser0const  10451  exp3vallem  10456  expnnval  10458  expp1  10462  expn1ap0  10465  mulexp  10494  expaddzaplem  10498  expaddzap  10499  expmul  10500  expp1zap  10504  expm1ap  10505  sqval  10513  iexpcyc  10559  subsq2  10562  qsqeqor  10565  binom2  10566  binom21  10567  binom2sub1  10569  mulbinom2  10571  binom3  10572  zesq  10573  bernneq  10575  sqoddm1div8  10608  nn0opthlem1d  10633  facp1  10643  faclbnd6  10657  bcval2  10663  bcval3  10664  bcn0  10668  bcp1n  10674  bcp1nk  10675  bcn2  10677  bcp1m1  10678  bcpasc  10679  bcn2m1  10682  hashinfom  10691  hashennn  10693  hashfz1  10696  fseq1hash  10714  omgadd  10715  hashunsng  10720  hashprg  10721  hashdifsn  10732  hashdifpr  10733  hashfz  10734  hashfzo  10735  hashfzo0  10736  hashfzp1  10737  hashfz0  10738  hashxp  10739  resunimafz0  10744  fnfz0hash  10745  ffzo0hash  10747  hashfacen  10749  zfz1isolemsplit  10751  zfz1isolemiso  10752  zfz1isolem1  10753  shftdm  10764  shftval2  10768  shftval4  10770  shftval5  10771  shftcan1  10776  seq3shft  10780  imre  10793  crre  10799  remim  10802  reim0b  10804  recj  10809  reneg  10810  readd  10811  resub  10812  remullem  10813  imcj  10817  imneg  10818  imadd  10819  imsub  10820  cjcj  10825  cjadd  10826  ipcnval  10828  cjneg  10832  cjsub  10834  cjexp  10835  imval2  10836  cjap  10848  resqrexlemf1  10950  resqrexlemfp1  10951  resqrexlemover  10952  resqrexlemcalc1  10956  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemcvg  10961  resqrtcl  10971  sqrtsq  10986  absneg  10992  absvalsq  10995  absvalsq2  10996  sqabsadd  10997  sqabssub  10998  absval2  10999  absreimsq  11009  absmul  11011  absexp  11021  absexpzap  11022  abssuble0  11045  abstri  11046  recan  11051  amgm2  11060  maxabslemlub  11149  max0addsup  11161  minmax  11171  minabs  11177  bdtrilem  11180  bdtri  11181  xrmaxiflemab  11188  xrmaxiflemcom  11190  xrmaxadd  11202  xrminmax  11206  xrmineqinf  11210  xrminrecl  11214  xrbdtri  11217  climshft2  11247  subcn2  11252  reccn2ap  11254  climaddc2  11271  iser3shft  11287  climcvg1nlem  11290  sumeq12dv  11313  sumeq12rdv  11314  sumrbdclem  11318  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  summodc  11324  fsum3  11328  isumz  11330  fsumf1o  11331  fisumss  11333  fsumsersdc  11336  fsum3ser  11338  fsumsplit  11348  fsumsplitf  11349  sumsnf  11350  fsumsplitsn  11351  fsum1  11353  sumpr  11354  sumtp  11355  fsumm1  11357  fsum1p  11359  fsumsplitsnun  11360  fsump1  11361  isumclim  11362  sumnul  11365  isumadd  11372  fsum2dlemstep  11375  fsumcnv  11378  fisumcom2  11379  fsumshftm  11386  fisumrev2  11387  fisum0diag2  11388  fsumsub  11393  fsumdifsnconst  11396  modfsummodlemstep  11398  fsumabs  11406  telfsumo  11407  telfsum  11409  telfsum2  11410  fsumparts  11411  fsumiun  11418  hashiun  11419  hash2iun  11420  hash2iun1dif1  11421  binomlem  11424  binom1p  11426  binom11  11427  binom1dif  11428  bcxmas  11430  isum1p  11433  isumnn0nn  11434  isumlessdc  11437  divcnv  11438  arisum2  11440  trireciplem  11441  geosergap  11447  geolim  11452  georeclim  11454  geo2lim  11457  geoisum1  11460  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemsumlt  11469  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodfrecap  11487  prodeq12dv  11510  prodeq12rdv  11511  prodrbdclem  11512  fproddccvg  11513  prodmodclem3  11516  prodmodclem2a  11517  zprodap0  11522  fprodseq  11524  fprodntrivap  11525  prod1dc  11527  fprodf1o  11529  prodssdc  11530  fprodssdc  11531  prodsnf  11533  fprod1  11535  fprodsplitdc  11537  fprodm1  11539  fprod1p  11540  fprodp1  11541  fprodunsn  11545  fprodcl2lem  11546  fprodabs  11557  fprodconst  11561  fprod2dlemstep  11563  fprodcnv  11566  fprodcom2fi  11567  fprodrec  11570  fprodsplitsn  11574  fprodsplit1f  11575  fprodeq0g  11579  eftabs  11597  efcllemp  11599  ef0lem  11601  efcvgfsum  11608  ege2le3  11612  efcj  11614  efaddlem  11615  efexp  11623  eftlub  11631  efsep  11632  effsumlt  11633  ef4p  11635  efgt1p2  11636  efgt1p  11637  tanval2ap  11654  tanval3ap  11655  resinval  11656  recosval  11657  efi4p  11658  resin4p  11659  recos4p  11660  sinneg  11667  cosneg  11668  tannegap  11669  efmival  11674  sinadd  11677  cosadd  11678  tanaddaplem  11679  tanaddap  11680  sinsub  11681  cossub  11682  addsin  11683  subsin  11684  subcos  11688  sincossq  11689  sin2t  11690  sin01bnd  11698  cos01bnd  11699  absefi  11709  absef  11710  absefib  11711  efieq1re  11712  demoivre  11713  demoivreALT  11714  eirraplem  11717  dvdstr  11768  dvdsadd2b  11780  mulmoddvds  11801  ltoddhalfle  11830  opoe  11832  m1expo  11837  m1exp1  11838  flodddiv4  11871  flodddiv4t2lthalf  11874  zsupcllemstep  11878  nn0gcdid0  11914  gcdaddm  11917  gcdadd  11918  gcdid  11919  gcdabs  11921  modgcd  11924  1gcd  11925  bezout  11944  dfgcd2  11947  mulgcd  11949  absmulgcd  11950  gcdmultiple  11953  gcdmultiplez  11954  rpmulgcd  11959  rplpwr  11960  rppwr  11961  dvdssqlem  11963  uzwodc  11970  ialgr0  11976  alginv  11979  algcvg  11980  algfx  11984  eucalginv  11988  eucalglt  11989  lcmcl  12004  lcmabs  12008  lcmgcdlem  12009  lcmdvds  12011  lcmgcdnn  12014  coprmdvds  12024  qredeq  12028  divgcdcoprm0  12033  divgcdcoprmex  12034  rpexp1i  12086  sqrt2irrlem  12093  sqpweven  12107  2sqpwodd  12108  sqrt2irraplemnn  12111  qmuldeneqnum  12127  nn0gcdsq  12132  numdensq  12134  nn0sqrtelqelz  12138  phibndlem  12148  dfphi2  12152  phiprmpw  12154  phiprm  12155  phimullem  12157  eulerthlem1  12159  eulerthlemh  12163  eulerthlemth  12164  eulerth  12165  prmdiv  12167  hashgcdlem  12170  phisum  12172  odzdvds  12177  vfermltl  12183  powm2modprm  12184  modprm0  12186  nnnn0modprm0  12187  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem4  12200  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem14  12209  pythagtriplem16  12211  pceulem  12226  pcval  12228  pczpre  12229  pcdiv  12234  pc1  12237  pcrec  12240  pcexp  12241  pcid  12255  pcneg  12256  pcgcd1  12259  pc2dvds  12261  difsqpwdvds  12269  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmpt2  12274  pcprod  12276  pcfac  12280  prmpwdvds  12285  pockthlem  12286  1arithlem2  12294  4sqlem9  12316  4sqlem4  12322  mul4sqlem  12323  ennnfonelemp1  12339  ennnfonelemhdmp1  12342  ennnfonelemss  12343  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemhom  12348  ennnfonelemnn0  12355  ctinfomlemom  12360  setsvala  12425  fvsetsid  12428  setsresg  12432  setscom  12434  setsslid  12444  ressid2  12454  ressval2  12455  restid2  12565  lidrididd  12613  grprinvd  12617  ntrval  12750  clsval  12751  cldcls  12754  neival  12783  resttop  12810  restco  12814  restabs  12815  resttopon2  12818  cnpval  12838  cnntr  12865  cnrest2  12876  upxp  12912  uptx  12914  cnmpt11  12923  cnmpt21  12931  psmetsym  12969  psmetres2  12973  xmetsym  13008  xmettxlem  13149  txmetcnp  13158  cnbl0  13174  cnblcld  13175  remetdval  13179  bl2ioo  13182  tgioo  13186  addcncntoplem  13191  divcnap  13195  fsumcncntop  13196  cncfmet  13219  cncfmptc  13222  addccncf  13226  negcncf  13228  mulcncflem  13230  ivthinclemlopn  13254  limcimolemlt  13273  cnplimcim  13276  cnplimclemr  13278  limccnp2lem  13285  limccnp2cntop  13286  dvfvalap  13290  dvconst  13301  dvaddxxbr  13305  dvmulxxbr  13306  dvcjbr  13312  dvexp  13315  dvrecap  13317  dvmptclx  13320  dvmptaddx  13321  dvmptmulx  13322  dvmptcmulcn  13323  dveflem  13327  dvef  13328  reeff1oleme  13333  sin0pilem1  13342  sin0pilem2  13343  efper  13368  sinperlem  13369  sinmpi  13376  cosmpi  13377  sinppi  13378  cosppi  13379  efimpi  13380  ptolemy  13385  sinq12gt0  13391  coseq0negpitopi  13397  tangtx  13399  abssinper  13407  cosq34lt1  13411  relogexp  13433  logdivlti  13442  logcxp  13458  rpcxp0  13459  rpcxp1  13460  1cxp  13461  ecxp  13462  rpcxpadd  13466  rpcxpp1  13467  rpmulcxp  13470  rpdivcxp  13472  cxpmul  13473  rpcxproot  13474  abscxp  13475  rpcxpsqrtth  13490  rplogbid1  13505  rplogb1  13506  rpelogb  13507  rplogbreexp  13511  rplogbzexp  13512  rprelogbmul  13513  rprelogbmulexp  13514  rprelogbdiv  13515  logbrec  13518  rpcxplogb  13522  logbgcd1irr  13525  logbgcd1irraplemexp  13526  logbgcd1irraplemap  13527  binom4  13537  lgslem1  13541  lgsval2lem  13551  lgsvalmod  13560  lgsneg  13565  lgsdir2lem4  13572  lgsdirprm  13575  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgsmodeq  13586  lgsdirnn0  13588  lgsdinn0  13589  2sqlem3  13593  2sqlem4  13594  2sqlem8  13599  djucllem  13681  bj-charfun  13689  bj-charfundc  13690  bj-charfundcALT  13691  nninfsellemeq  13894  nninffeq  13900  qdencn  13906  cvgcmp2nlemabs  13911  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  apdifflemf  13925  redcwlpolemeq1  13933  dceqnconst  13938  dcapnconst  13939  nconstwlpolem0  13941  nconstwlpolemgt0  13942  nconstwlpolem  13943
  Copyright terms: Public domain W3C validator