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

Theorem eqtrd 2173
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 2152 . 2 (𝜑 → (𝐴 = 𝐵𝐴 = 𝐶))
41, 3mpbid 146 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  eqtr2d  2174  eqtr3d  2175  eqtr4d  2176  3eqtrd  2177  3eqtrrd  2178  3eqtr2d  2179  syl5eq  2185  eqtrdi  2189  rabeqbidv  2684  rabeqbidva  2685  csbidmg  3060  csbco3g  3062  difeq12d  3199  ifeq12d  3495  ifbieq1d  3498  ifbieq2d  3500  ifbieq12d  3502  eqifdc  3510  csbsng  3591  disjpr2  3594  csbunig  3751  iuneq12d  3844  unisn3  4373  op1stbg  4407  opthreg  4478  onsucuni2  4486  csbxpg  4627  coeq12d  4710  csbdmg  4740  reseq12d  4827  csbresg  4829  resima2  4860  imaeq12d  4889  csbrng  5007  opswapg  5032  relcnvtr  5065  relcoi2  5076  relcoi1  5077  iotaint  5108  funprg  5180  funtpg  5181  funcnvres2  5205  fnco  5238  fococnv2  5400  fveq12d  5435  csbfv12g  5464  csbfv2g  5465  csbfvg  5466  dffn5im  5474  funfvdm2  5492  fvun1  5494  fvmpt2d  5514  fvmptt  5519  fndmin  5534  fniniseg2  5549  fnniniseg2  5550  fmptcof  5594  fvresi  5620  fvunsng  5621  fvpr1g  5633  fvpr2g  5634  fvtp1g  5635  funiunfvdm  5671  fcof1o  5697  riotaeqbidv  5740  oveq123d  5802  csbov12g  5817  csbov1g  5818  csbov2g  5819  ovmpodxf  5903  caov42d  5964  caovdilemd  5969  caovimo  5971  grprinvd  5973  offeq  6002  offval2  6004  caofinvl  6011  ot1stg  6057  ot2ndg  6058  2nd1st  6085  mpomptsx  6102  dmmpossx  6104  fmpox  6105  fmpoco  6120  1stconst  6125  algrflemg  6134  tfrexlem  6238  rdgivallem  6285  rdgisuc1  6288  frec0g  6301  frecabcl  6303  frecsuclem  6310  frecrdg  6312  oa0  6360  oasuc  6367  oa1suc  6370  omsuc  6375  nnaass  6388  nndi  6389  nnmass  6390  nnm2  6428  nn2m  6429  ereq1  6443  errn  6458  uniqs2  6496  oviec  6542  ecovass  6545  ecoviass  6546  ecovdi  6547  ecovidi  6548  mapsnconst  6595  mapen  6747  mapxpen  6749  xpmapenlem  6750  phplem4on  6768  fidifsnen  6771  undifdc  6819  fiintim  6824  fisseneq  6827  snexxph  6845  sbthlemi4  6855  sbthlemi6  6857  supeq2  6883  eqsupti  6890  infvalti  6916  djuf1olem  6945  djuss  6962  1stinl  6966  2ndinl  6967  1stinr  6968  2ndinr  6969  updjudhcoinlf  6972  updjudhcoinrg  6973  omp1eomlem  6986  difinfsn  6992  ctmlemr  7000  ctssdclemn0  7002  ctssdc  7005  enumctlemm  7006  enwomnilem  7049  en2other2  7068  cc3  7099  mulidpi  7149  addasspig  7161  mulasspig  7163  distrpig  7164  indpi  7173  addcmpblnq  7198  mulpipq  7203  dmaddpqlem  7208  nqpi  7209  addcomnqg  7212  recrecnq  7225  ltsonq  7229  ltanqg  7231  ltmnqg  7232  ltaddnq  7238  ltexnqq  7239  archnqq  7248  prarloclemarch  7249  ltrnqg  7251  ltnnnq  7254  nq0nn  7273  addcmpblnq0  7274  nqpnq0nq  7284  nqnq0a  7285  nq0m0r  7287  nq0a0  7288  distrnq0  7290  addassnq0  7293  nq02m  7296  prarloclemlo  7325  prarloclemcalc  7333  addnqprllem  7358  addnqprulem  7359  addnqprl  7360  addnqpru  7361  appdivnq  7394  mulnqprl  7399  mulnqpru  7400  addcanprlemu  7446  ltaprlem  7449  ltmprr  7473  cauappcvgprlemladdrl  7488  mulcmpblnrlemg  7571  mulcomsrg  7588  distrsrg  7590  ltsosr  7595  1idsr  7599  00sr  7600  ltasrg  7601  recexgt0sr  7604  srpospr  7614  prsradd  7617  prsrriota  7619  caucvgsrlemcau  7624  caucvgsrlemgt1  7626  caucvgsrlemoffval  7627  caucvgsrlemoffres  7631  caucvgsr  7633  map2psrprg  7636  elreal2  7661  mulresr  7669  pitonnlem1p1  7677  pitonnlem2  7678  pitoregt0  7680  recidpirqlemcalc  7688  recidpirq  7689  axaddcl  7695  axmulcl  7697  axmulcom  7702  axmulass  7704  axdistr  7705  ax1rid  7708  axcnre  7712  recriota  7721  axcaucvglemcau  7729  mulid1  7786  mulid2  7787  adddirp1d  7815  joinlmuladdmuld  7816  muladd11  7918  1p1times  7919  readdcan  7925  comraddd  7942  add42  7947  npcan  7994  addsubass  7995  2addsub  7999  addsubeq4  8000  nppcan  8007  nnpcan  8008  npncan2  8012  nncan  8014  subsub  8015  nnncan  8020  nnncan1  8021  pnpcan2  8025  pnncan  8026  subneg  8034  negneg  8035  negdi2  8043  mvrraddd  8151  assraddsubd  8153  subaddeqd  8154  addid0  8158  mul02  8172  mul01  8174  mulneg1  8180  mul2neg  8183  mulm1  8185  ltadd2  8204  rimul  8370  rereim  8371  mulreim  8389  recextlem1  8435  mulcanapd  8445  divcanap1  8464  divrecap2  8472  divmulassap  8478  divmulasscomap  8479  divcanap4  8482  dividap  8484  muldivdirap  8490  divdivdivap  8496  recdivap  8501  divadddivap  8510  divsubdivap  8511  div2negap  8518  divcanap5rd  8601  dmdcanap2d  8604  subrecap  8621  recgt0  8631  lt2mul2div  8660  nnmulcl  8764  times2  8872  add1p1  8992  sub1m1  8993  cnm2m1cnm3  8994  nn0supp  9052  peano2z  9113  nneoor  9176  supminfex  9418  cnref1o  9468  rexneg  9642  xaddpnf1  9658  xaddmnf1  9660  rexadd  9664  xaddid1  9674  xaddid2  9675  xaddass  9681  xpncan  9683  xleadd1a  9685  xltadd1  9688  xposdif  9694  xadd4d  9697  xleaddadd  9699  iooidg  9721  iooval2  9727  icoshftf1o  9803  lincmb01cmp  9815  iccf1o  9816  fzval2  9823  fzsuc  9879  fzpred  9880  fztpval  9893  fseq1p1m1  9904  fzshftral  9918  fzo0to3tp  10026  fzo0sn0fzo1  10028  fzosplitsn  10040  fzosplitprm1  10041  fzisfzounsn  10043  rebtwn2zlemstep  10060  2tnp1ge0ge0  10104  flqdiv  10124  modqvalr  10128  modqdiffl  10138  modqfrac  10140  modqmulnn  10145  modqid  10152  modqcyc  10162  modqcyc2  10163  mulp1mod1  10168  modqmuladd  10169  modqmuladdnn0  10171  qnegmod  10172  m1modnnsub1  10173  addmodid  10175  addmodidr  10176  modqmul12d  10181  modqnegd  10182  modqadd12d  10183  modifeq2int  10189  modqaddmulmod  10194  modqdi  10195  modqsubdir  10196  modsumfzodifsn  10199  addmodlteq  10201  frec2uzsucd  10204  frecuzrdgrrn  10211  frec2uzrdg  10212  frecuzrdglem  10214  frecuzrdgsuc  10217  frecuzrdgg  10219  frecuzrdgdomlem  10220  frecuzrdgfunlem  10222  frecuzrdgtclt  10224  frecuzrdgsuctlem  10226  frecfzennn  10229  seqeq1  10251  seq3val  10261  seqvalcd  10262  seq3p1  10265  seqp1cd  10269  seq3feq2  10273  seq3fveq  10274  seq3shft2  10276  seq3-1p  10283  iseqf1olemnab  10291  iseqf1olemab  10292  iseqf1olemnanb  10293  iseqf1olemqk  10297  iseqf1olemfvp  10300  seq3f1olemqsumkj  10301  seq3f1olemqsumk  10302  seq3f1olemqsum  10303  seq3f1o  10307  seq3id3  10310  seq3z  10314  fser0const  10319  exp3vallem  10324  expnnval  10326  expp1  10330  expn1ap0  10333  mulexp  10362  expaddzaplem  10366  expaddzap  10367  expmul  10368  expp1zap  10372  expm1ap  10373  sqval  10381  iexpcyc  10427  subsq2  10430  binom2  10433  binom21  10434  binom2sub1  10436  mulbinom2  10438  binom3  10439  zesq  10440  bernneq  10442  sqoddm1div8  10474  nn0opthlem1d  10497  facp1  10507  faclbnd6  10521  bcval2  10527  bcval3  10528  bcn0  10532  bcp1n  10538  bcp1nk  10539  bcn2  10541  bcp1m1  10542  bcpasc  10543  bcn2m1  10546  hashinfom  10555  hashennn  10557  hashfz1  10560  fseq1hash  10578  omgadd  10579  hashunsng  10584  hashprg  10585  hashdifsn  10596  hashdifpr  10597  hashfz  10598  hashfzo  10599  hashfzo0  10600  hashfzp1  10601  hashfz0  10602  hashxp  10603  resunimafz0  10605  fnfz0hash  10606  ffzo0hash  10608  hashfacen  10610  zfz1isolemsplit  10612  zfz1isolemiso  10613  zfz1isolem1  10614  shftdm  10625  shftval2  10629  shftval4  10631  shftval5  10632  shftcan1  10637  seq3shft  10641  imre  10654  crre  10660  remim  10663  reim0b  10665  recj  10670  reneg  10671  readd  10672  resub  10673  remullem  10674  imcj  10678  imneg  10679  imadd  10680  imsub  10681  cjcj  10686  cjadd  10687  ipcnval  10689  cjneg  10693  cjsub  10695  cjexp  10696  imval2  10697  cjap  10709  resqrexlemf1  10811  resqrexlemfp1  10812  resqrexlemover  10813  resqrexlemcalc1  10817  resqrexlemcalc3  10819  resqrexlemnm  10821  resqrexlemcvg  10822  resqrtcl  10832  sqrtsq  10847  absneg  10853  absvalsq  10856  absvalsq2  10857  sqabsadd  10858  sqabssub  10859  absval2  10860  absreimsq  10870  absmul  10872  absexp  10882  absexpzap  10883  abssuble0  10906  abstri  10907  recan  10912  amgm2  10921  maxabslemlub  11010  max0addsup  11022  minmax  11032  minabs  11038  bdtrilem  11041  bdtri  11042  xrmaxiflemab  11047  xrmaxiflemcom  11049  xrmaxadd  11061  xrminmax  11065  xrmineqinf  11069  xrminrecl  11073  xrbdtri  11076  climshft2  11106  subcn2  11111  reccn2ap  11113  climaddc2  11130  iser3shft  11146  climcvg1nlem  11149  sumeq12dv  11172  sumeq12rdv  11173  sumrbdclem  11177  fsum3cvg  11178  summodclem3  11180  summodclem2a  11181  summodc  11183  fsum3  11187  isumz  11189  fsumf1o  11190  fisumss  11192  fsumsersdc  11195  fsum3ser  11197  fsumsplit  11207  fsumsplitf  11208  sumsnf  11209  fsumsplitsn  11210  fsum1  11212  sumpr  11213  sumtp  11214  fsumm1  11216  fsum1p  11218  fsumsplitsnun  11219  fsump1  11220  isumclim  11221  sumnul  11224  isumadd  11231  fsum2dlemstep  11234  fsumcnv  11237  fisumcom2  11238  fsumshftm  11245  fisumrev2  11246  fisum0diag2  11247  fsumsub  11252  fsumdifsnconst  11255  modfsummodlemstep  11257  fsumabs  11265  telfsumo  11266  telfsum  11268  telfsum2  11269  fsumparts  11270  fsumiun  11277  hashiun  11278  hash2iun  11279  hash2iun1dif1  11280  binomlem  11283  binom1p  11285  binom11  11286  binom1dif  11287  bcxmas  11289  isum1p  11292  isumnn0nn  11293  isumlessdc  11296  divcnv  11297  arisum2  11299  trireciplem  11300  geosergap  11306  geolim  11311  georeclim  11313  geo2lim  11316  geoisum1  11319  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  cvgratnnlemsumlt  11328  cvgratz  11332  mertenslemi1  11335  mertenslem2  11336  mertensabs  11337  prodfrecap  11346  prodeq12dv  11369  prodeq12rdv  11370  prodrbdclem  11371  fproddccvg  11372  prodmodclem3  11375  prodmodclem2a  11376  zprodap0  11381  eftabs  11397  efcllemp  11399  ef0lem  11401  efcvgfsum  11408  ege2le3  11412  efcj  11414  efaddlem  11415  efexp  11423  eftlub  11431  efsep  11432  effsumlt  11433  ef4p  11435  efgt1p2  11436  efgt1p  11437  tanval2ap  11454  tanval3ap  11455  resinval  11456  recosval  11457  efi4p  11458  resin4p  11459  recos4p  11460  sinneg  11467  cosneg  11468  tannegap  11469  efmival  11474  sinadd  11477  cosadd  11478  tanaddaplem  11479  tanaddap  11480  sinsub  11481  cossub  11482  addsin  11483  subsin  11484  subcos  11488  sincossq  11489  sin2t  11490  sin01bnd  11498  cos01bnd  11499  absefi  11509  absef  11510  absefib  11511  efieq1re  11512  demoivre  11513  demoivreALT  11514  eirraplem  11517  dvdstr  11564  dvdsadd2b  11574  mulmoddvds  11595  ltoddhalfle  11624  opoe  11626  m1expo  11631  m1exp1  11632  flodddiv4  11665  flodddiv4t2lthalf  11668  zsupcllemstep  11672  nn0gcdid0  11703  gcdaddm  11706  gcdadd  11707  gcdid  11708  gcdabs  11710  modgcd  11713  1gcd  11714  bezout  11733  dfgcd2  11736  mulgcd  11738  absmulgcd  11739  gcdmultiple  11742  gcdmultiplez  11743  rpmulgcd  11748  rplpwr  11749  rppwr  11750  dvdssqlem  11752  ialgr0  11759  alginv  11762  algcvg  11763  algfx  11767  eucalginv  11771  eucalglt  11772  lcmcl  11787  lcmabs  11791  lcmgcdlem  11792  lcmdvds  11794  lcmgcdnn  11797  coprmdvds  11807  qredeq  11811  divgcdcoprm0  11816  divgcdcoprmex  11817  rpexp1i  11866  sqrt2irrlem  11873  sqpweven  11887  2sqpwodd  11888  sqrt2irraplemnn  11891  qmuldeneqnum  11907  nn0gcdsq  11912  numdensq  11914  nn0sqrtelqelz  11918  phibndlem  11926  dfphi2  11930  phiprmpw  11932  phiprm  11933  phimullem  11935  hashgcdlem  11937  ennnfonelemp1  11953  ennnfonelemhdmp1  11956  ennnfonelemss  11957  ennnfonelemkh  11959  ennnfonelemhf1o  11960  ennnfonelemhom  11962  ennnfonelemnn0  11969  ctinfomlemom  11974  setsvala  12027  fvsetsid  12030  setsresg  12034  setscom  12036  setsslid  12046  ressid2  12055  ressval2  12056  restid2  12166  ntrval  12316  clsval  12317  cldcls  12320  neival  12349  resttop  12376  restco  12380  restabs  12381  resttopon2  12384  cnpval  12404  cnntr  12431  cnrest2  12442  upxp  12478  uptx  12480  cnmpt11  12489  cnmpt21  12497  psmetsym  12535  psmetres2  12539  xmetsym  12574  xmettxlem  12715  txmetcnp  12724  cnbl0  12740  cnblcld  12741  remetdval  12745  bl2ioo  12748  tgioo  12752  addcncntoplem  12757  divcnap  12761  fsumcncntop  12762  cncfmet  12785  cncfmptc  12788  addccncf  12792  negcncf  12794  mulcncflem  12796  ivthinclemlopn  12820  limcimolemlt  12839  cnplimcim  12842  cnplimclemr  12844  limccnp2lem  12851  limccnp2cntop  12852  dvfvalap  12856  dvconst  12867  dvaddxxbr  12871  dvmulxxbr  12872  dvcjbr  12878  dvexp  12881  dvrecap  12883  dvmptclx  12886  dvmptaddx  12887  dvmptmulx  12888  dvmptcmulcn  12889  dveflem  12893  dvef  12894  reeff1oleme  12899  sin0pilem1  12908  sin0pilem2  12909  efper  12934  sinperlem  12935  sinmpi  12942  cosmpi  12943  sinppi  12944  cosppi  12945  efimpi  12946  ptolemy  12951  sinq12gt0  12957  coseq0negpitopi  12963  tangtx  12965  abssinper  12973  cosq34lt1  12977  relogexp  12999  logdivlti  13008  logcxp  13024  rpcxp0  13025  rpcxp1  13026  1cxp  13027  ecxp  13028  rpcxpadd  13032  rpcxpp1  13033  rpmulcxp  13036  rpdivcxp  13038  cxpmul  13039  rpcxproot  13040  abscxp  13041  rpcxpsqrtth  13056  rplogbid1  13070  rplogb1  13071  rpelogb  13072  rplogbreexp  13076  rplogbzexp  13077  rprelogbmul  13078  rprelogbmulexp  13079  rprelogbdiv  13080  logbrec  13083  rpcxplogb  13087  logbgcd1irr  13090  logbgcd1irraplemexp  13091  logbgcd1irraplemap  13092  djucllem  13176  nninfalllemn  13375  nninfsellemeq  13383  nninffeq  13389  qdencn  13395  cvgcmp2nlemabs  13400  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  apdifflemf  13412  redcwlpolemeq1  13419  dcapncf  13421
  Copyright terms: Public domain W3C validator