Theorem eqtrd 2203

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

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eqeq2d 2182	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  eqtr2d  2204  eqtr3d  2205  eqtr4d  2206  3eqtrd  2207  3eqtrrd  2208  3eqtr2d  2209  eqtrid  2215  eqtrdi  2219  rabeqbidv  2725  rabeqbidva  2726  csbidmg  3105  csbco3g  3107  difeq12d  3246  ifeq12d  3544  ifbieq1d  3547  ifbieq2d  3549  ifbieq12d  3551  eqifdc  3559  csbsng  3642  disjpr2  3645  csbunig  3802  iuneq12d  3895  unisn3  4428  op1stbg  4462  opthreg  4538  onsucuni2  4546  csbxpg  4690  coeq12d  4773  csbdmg  4803  reseq12d  4890  csbresg  4892  resima2  4923  imaeq12d  4952  csbrng  5070  opswapg  5095  relcnvtr  5128  relcoi2  5139  relcoi1  5140  iotaint  5171  funprg  5246  funtpg  5247  funcnvres2  5271  fnco  5304  fococnv2  5466  fveq12d  5501  csbfv12g  5530  csbfv2g  5531  csbfvg  5532  dffn5im  5540  funfvdm2  5558  fvun1  5560  fvmpt2d  5580  fvmptt  5585  fndmin  5600  fniniseg2  5615  fnniniseg2  5616  fmptcof  5660  fvresi  5686  fvunsng  5687  fvpr1g  5699  fvpr2g  5700  fvtp1g  5701  funiunfvdm  5739  fcof1o  5765  riotaeqbidv  5809  oveq123d  5871  csbov12g  5889  csbov1g  5890  csbov2g  5891  ovmpodxf  5975  caov42d  6036  caovdilemd  6041  caovimo  6043  offeq  6071  offval2  6073  caofinvl  6080  ot1stg  6128  ot2ndg  6129  2nd1st  6156  mpomptsx  6173  dmmpossx  6175  fmpox  6176  fmpoco  6192  1stconst  6197  algrflemg  6206  tfrexlem  6310  rdgivallem  6357  rdgisuc1  6360  frec0g  6373  frecabcl  6375  frecsuclem  6382  frecrdg  6384  oa0  6433  oasuc  6440  oa1suc  6443  omsuc  6448  nnaass  6461  nndi  6462  nnmass  6463  nnm2  6501  nn2m  6502  ereq1  6516  errn  6531  uniqs2  6569  oviec  6615  ecovass  6618  ecoviass  6619  ecovdi  6620  ecovidi  6621  mapsnconst  6668  mapen  6820  mapxpen  6822  xpmapenlem  6823  phplem4on  6841  fidifsnen  6844  undifdc  6897  fiintim  6902  fisseneq  6905  snexxph  6923  sbthlemi4  6933  sbthlemi6  6935  supeq2  6962  eqsupti  6969  infvalti  6995  djuf1olem  7026  djuss  7043  1stinl  7047  2ndinl  7048  1stinr  7049  2ndinr  7050  updjudhcoinlf  7053  updjudhcoinrg  7054  omp1eomlem  7067  difinfsn  7073  ctmlemr  7081  ctssdclemn0  7083  ctssdc  7086  enumctlemm  7087  nnnninfeq  7100  nnnninfeq2  7101  nninfisollemne  7103  nninfisol  7105  enwomnilem  7141  en2other2  7160  cc3  7217  mulidpi  7267  addasspig  7279  mulasspig  7281  distrpig  7282  indpi  7291  addcmpblnq  7316  mulpipq  7321  dmaddpqlem  7326  nqpi  7327  addcomnqg  7330  recrecnq  7343  ltsonq  7347  ltanqg  7349  ltmnqg  7350  ltaddnq  7356  ltexnqq  7357  archnqq  7366  prarloclemarch  7367  ltrnqg  7369  ltnnnq  7372  nq0nn  7391  addcmpblnq0  7392  nqpnq0nq  7402  nqnq0a  7403  nq0m0r  7405  nq0a0  7406  distrnq0  7408  addassnq0  7411  nq02m  7414  prarloclemlo  7443  prarloclemcalc  7451  addnqprllem  7476  addnqprulem  7477  addnqprl  7478  addnqpru  7479  appdivnq  7512  mulnqprl  7517  mulnqpru  7518  addcanprlemu  7564  ltaprlem  7567  ltmprr  7591  cauappcvgprlemladdrl  7606  mulcmpblnrlemg  7689  mulcomsrg  7706  distrsrg  7708  ltsosr  7713  1idsr  7717  00sr  7718  ltasrg  7719  recexgt0sr  7722  srpospr  7732  prsradd  7735  prsrriota  7737  caucvgsrlemcau  7742  caucvgsrlemgt1  7744  caucvgsrlemoffval  7745  caucvgsrlemoffres  7749  caucvgsr  7751  map2psrprg  7754  elreal2  7779  mulresr  7787  pitonnlem1p1  7795  pitonnlem2  7796  pitoregt0  7798  recidpirqlemcalc  7806  recidpirq  7807  axaddcl  7813  axmulcl  7815  axmulcom  7820  axmulass  7822  axdistr  7823  ax1rid  7826  axcnre  7830  recriota  7839  axcaucvglemcau  7847  mulid1  7904  mulid2  7905  adddirp1d  7933  joinlmuladdmuld  7934  muladd11  8039  1p1times  8040  readdcan  8046  comraddd  8063  add42  8068  npcan  8115  addsubass  8116  2addsub  8120  addsubeq4  8121  nppcan  8128  nnpcan  8129  npncan2  8133  nncan  8135  subsub  8136  nnncan  8141  nnncan1  8142  pnpcan2  8146  pnncan  8147  subneg  8155  negneg  8156  negdi2  8164  mvrraddd  8272  assraddsubd  8274  subaddeqd  8275  addid0  8279  mul02  8293  mul01  8295  mulneg1  8301  mul2neg  8304  mulm1  8306  ltadd2  8325  rimul  8491  rereim  8492  mulreim  8510  recextlem1  8556  mulcanapd  8566  divcanap1  8585  divrecap2  8593  divmulassap  8599  divmulasscomap  8600  divcanap4  8603  dividap  8605  muldivdirap  8611  divdivdivap  8617  recdivap  8622  divadddivap  8631  divsubdivap  8632  div2negap  8639  divcanap5rd  8722  dmdcanap2d  8725  subrecap  8743  recgt0  8753  lt2mul2div  8782  nnmulcl  8886  times2  8994  add1p1  9114  sub1m1  9115  cnm2m1cnm3  9116  nn0supp  9174  peano2z  9235  nneoor  9301  supminfex  9543  cnref1o  9596  rexneg  9774  xaddpnf1  9790  xaddmnf1  9792  rexadd  9796  xaddid1  9806  xaddid2  9807  xaddass  9813  xpncan  9815  xleadd1a  9817  xltadd1  9820  xposdif  9826  xadd4d  9829  xleaddadd  9831  iooidg  9853  iooval2  9859  icoshftf1o  9935  lincmb01cmp  9947  iccf1o  9948  fzval2  9955  fzsuc  10012  fzpred  10013  fztpval  10026  fseq1p1m1  10037  fzshftral  10051  fz0to4untppr  10067  fzo0to3tp  10162  fzo0sn0fzo1  10164  fzosplitsn  10176  fzosplitprm1  10177  fzisfzounsn  10179  rebtwn2zlemstep  10196  2tnp1ge0ge0  10244  flqdiv  10264  modqvalr  10268  modqdiffl  10278  modqfrac  10280  modqmulnn  10285  modqid  10292  modqcyc  10302  modqcyc2  10303  mulp1mod1  10308  modqmuladd  10309  modqmuladdnn0  10311  qnegmod  10312  m1modnnsub1  10313  addmodid  10315  addmodidr  10316  modqmul12d  10321  modqnegd  10322  modqadd12d  10323  modifeq2int  10329  modqaddmulmod  10334  modqdi  10335  modqsubdir  10336  modsumfzodifsn  10339  addmodlteq  10341  frec2uzsucd  10344  frecuzrdgrrn  10351  frec2uzrdg  10352  frecuzrdglem  10354  frecuzrdgsuc  10357  frecuzrdgg  10359  frecuzrdgdomlem  10360  frecuzrdgfunlem  10362  frecuzrdgtclt  10364  frecuzrdgsuctlem  10366  frecfzennn  10369  seqeq1  10391  seq3val  10401  seqvalcd  10402  seq3p1  10405  seqp1cd  10409  seq3feq2  10413  seq3fveq  10414  seq3shft2  10416  seq3-1p  10423  iseqf1olemnab  10431  iseqf1olemab  10432  iseqf1olemnanb  10433  iseqf1olemqk  10437  iseqf1olemfvp  10440  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  seq3f1o  10447  seq3id3  10450  seq3z  10454  fser0const  10459  exp3vallem  10464  expnnval  10466  expp1  10470  expn1ap0  10473  mulexp  10502  expaddzaplem  10506  expaddzap  10507  expmul  10508  expp1zap  10512  expm1ap  10513  sqval  10521  iexpcyc  10567  subsq2  10570  qsqeqor  10573  binom2  10574  binom21  10575  binom2sub1  10577  mulbinom2  10579  binom3  10580  zesq  10581  bernneq  10583  sqoddm1div8  10616  nn0opthlem1d  10641  facp1  10651  faclbnd6  10665  bcval2  10671  bcval3  10672  bcn0  10676  bcp1n  10682  bcp1nk  10683  bcn2  10685  bcp1m1  10686  bcpasc  10687  bcn2m1  10690  hashinfom  10699  hashennn  10701  hashfz1  10704  fseq1hash  10723  omgadd  10724  hashunsng  10729  hashprg  10730  hashdifsn  10741  hashdifpr  10742  hashfz  10743  hashfzo  10744  hashfzo0  10745  hashfzp1  10746  hashfz0  10747  hashxp  10748  resunimafz0  10753  fnfz0hash  10754  ffzo0hash  10756  hashfacen  10758  zfz1isolemsplit  10760  zfz1isolemiso  10761  zfz1isolem1  10762  shftdm  10773  shftval2  10777  shftval4  10779  shftval5  10780  shftcan1  10785  seq3shft  10789  imre  10802  crre  10808  remim  10811  reim0b  10813  recj  10818  reneg  10819  readd  10820  resub  10821  remullem  10822  imcj  10826  imneg  10827  imadd  10828  imsub  10829  cjcj  10834  cjadd  10835  ipcnval  10837  cjneg  10841  cjsub  10843  cjexp  10844  imval2  10845  cjap  10857  resqrexlemf1  10959  resqrexlemfp1  10960  resqrexlemover  10961  resqrexlemcalc1  10965  resqrexlemcalc3  10967  resqrexlemnm  10969  resqrexlemcvg  10970  resqrtcl  10980  sqrtsq  10995  absneg  11001  absvalsq  11004  absvalsq2  11005  sqabsadd  11006  sqabssub  11007  absval2  11008  absreimsq  11018  absmul  11020  absexp  11030  absexpzap  11031  abssuble0  11054  abstri  11055  recan  11060  amgm2  11069  maxabslemlub  11158  max0addsup  11170  minmax  11180  minabs  11186  bdtrilem  11189  bdtri  11190  xrmaxiflemab  11197  xrmaxiflemcom  11199  xrmaxadd  11211  xrminmax  11215  xrmineqinf  11219  xrminrecl  11223  xrbdtri  11226  climshft2  11256  subcn2  11261  reccn2ap  11263  climaddc2  11280  iser3shft  11296  climcvg1nlem  11299  sumeq12dv  11322  sumeq12rdv  11323  sumrbdclem  11327  fsum3cvg  11328  summodclem3  11330  summodclem2a  11331  summodc  11333  fsum3  11337  isumz  11339  fsumf1o  11340  fisumss  11342  fsumsersdc  11345  fsum3ser  11347  fsumsplit  11357  fsumsplitf  11358  sumsnf  11359  fsumsplitsn  11360  fsum1  11362  sumpr  11363  sumtp  11364  fsumm1  11366  fsum1p  11368  fsumsplitsnun  11369  fsump1  11370  isumclim  11371  sumnul  11374  isumadd  11381  fsum2dlemstep  11384  fsumcnv  11387  fisumcom2  11388  fsumshftm  11395  fisumrev2  11396  fisum0diag2  11397  fsumsub  11402  fsumdifsnconst  11405  modfsummodlemstep  11407  fsumabs  11415  telfsumo  11416  telfsum  11418  telfsum2  11419  fsumparts  11420  fsumiun  11427  hashiun  11428  hash2iun  11429  hash2iun1dif1  11430  binomlem  11433  binom1p  11435  binom11  11436  binom1dif  11437  bcxmas  11439  isum1p  11442  isumnn0nn  11443  isumlessdc  11446  divcnv  11447  arisum2  11449  trireciplem  11450  geosergap  11456  geolim  11461  georeclim  11463  geo2lim  11466  geoisum1  11469  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  cvgratnnlemsumlt  11478  cvgratz  11482  mertenslemi1  11485  mertenslem2  11486  mertensabs  11487  prodfrecap  11496  prodeq12dv  11519  prodeq12rdv  11520  prodrbdclem  11521  fproddccvg  11522  prodmodclem3  11525  prodmodclem2a  11526  zprodap0  11531  fprodseq  11533  fprodntrivap  11534  prod1dc  11536  fprodf1o  11538  prodssdc  11539  fprodssdc  11540  prodsnf  11542  fprod1  11544  fprodsplitdc  11546  fprodm1  11548  fprod1p  11549  fprodp1  11550  fprodunsn  11554  fprodcl2lem  11555  fprodabs  11566  fprodconst  11570  fprod2dlemstep  11572  fprodcnv  11575  fprodcom2fi  11576  fprodrec  11579  fprodsplitsn  11583  fprodsplit1f  11584  fprodeq0g  11588  eftabs  11606  efcllemp  11608  ef0lem  11610  efcvgfsum  11617  ege2le3  11621  efcj  11623  efaddlem  11624  efexp  11632  eftlub  11640  efsep  11641  effsumlt  11642  ef4p  11644  efgt1p2  11645  efgt1p  11646  tanval2ap  11663  tanval3ap  11664  resinval  11665  recosval  11666  efi4p  11667  resin4p  11668  recos4p  11669  sinneg  11676  cosneg  11677  tannegap  11678  efmival  11683  sinadd  11686  cosadd  11687  tanaddaplem  11688  tanaddap  11689  sinsub  11690  cossub  11691  addsin  11692  subsin  11693  subcos  11697  sincossq  11698  sin2t  11699  sin01bnd  11707  cos01bnd  11708  absefi  11718  absef  11719  absefib  11720  efieq1re  11721  demoivre  11722  demoivreALT  11723  eirraplem  11726  dvdstr  11777  dvdsadd2b  11789  mulmoddvds  11810  ltoddhalfle  11839  opoe  11841  m1expo  11846  m1exp1  11847  flodddiv4  11880  flodddiv4t2lthalf  11883  zsupcllemstep  11887  nn0gcdid0  11923  gcdaddm  11926  gcdadd  11927  gcdid  11928  gcdabs  11930  modgcd  11933  1gcd  11934  bezout  11953  dfgcd2  11956  mulgcd  11958  absmulgcd  11959  gcdmultiple  11962  gcdmultiplez  11963  rpmulgcd  11968  rplpwr  11969  rppwr  11970  dvdssqlem  11972  uzwodc  11979  ialgr0  11985  alginv  11988  algcvg  11989  algfx  11993  eucalginv  11997  eucalglt  11998  lcmcl  12013  lcmabs  12017  lcmgcdlem  12018  lcmdvds  12020  lcmgcdnn  12023  coprmdvds  12033  qredeq  12037  divgcdcoprm0  12042  divgcdcoprmex  12043  rpexp1i  12095  sqrt2irrlem  12102  sqpweven  12116  2sqpwodd  12117  sqrt2irraplemnn  12120  qmuldeneqnum  12136  nn0gcdsq  12141  numdensq  12143  nn0sqrtelqelz  12147  phibndlem  12157  dfphi2  12161  phiprmpw  12163  phiprm  12164  phimullem  12166  eulerthlem1  12168  eulerthlemh  12172  eulerthlemth  12173  eulerth  12174  prmdiv  12176  hashgcdlem  12179  phisum  12181  odzdvds  12186  vfermltl  12192  powm2modprm  12193  modprm0  12195  nnnn0modprm0  12196  coprimeprodsq  12198  pythagtriplem1  12206  pythagtriplem3  12208  pythagtriplem4  12209  pythagtriplem6  12211  pythagtriplem7  12212  pythagtriplem14  12218  pythagtriplem16  12220  pceulem  12235  pcval  12237  pczpre  12238  pcdiv  12243  pc1  12246  pcrec  12249  pcexp  12250  pcid  12264  pcneg  12265  pcgcd1  12268  pc2dvds  12270  difsqpwdvds  12278  pcaddlem  12279  pcadd  12280  pcmpt  12282  pcmpt2  12283  pcprod  12285  pcfac  12289  prmpwdvds  12294  pockthlem  12295  1arithlem2  12303  4sqlem9  12325  4sqlem4  12331  mul4sqlem  12332  ennnfonelemp1  12348  ennnfonelemhdmp1  12351  ennnfonelemss  12352  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemhom  12357  ennnfonelemnn0  12364  ctinfomlemom  12369  setsvala  12434  fvsetsid  12437  setsresg  12441  setscom  12443  setsslid  12453  ressid2  12463  ressval2  12464  restid2  12574  lidrididd  12622  grprinvd  12626  mndpropd  12662  mhmf1o  12679  mhmco  12691  ntrval  12825  clsval  12826  cldcls  12829  neival  12858  resttop  12885  restco  12889  restabs  12890  resttopon2  12893  cnpval  12913  cnntr  12940  cnrest2  12951  upxp  12987  uptx  12989  cnmpt11  12998  cnmpt21  13006  psmetsym  13044  psmetres2  13048  xmetsym  13083  xmettxlem  13224  txmetcnp  13233  cnbl0  13249  cnblcld  13250  remetdval  13254  bl2ioo  13257  tgioo  13261  addcncntoplem  13266  divcnap  13270  fsumcncntop  13271  cncfmet  13294  cncfmptc  13297  addccncf  13301  negcncf  13303  mulcncflem  13305  ivthinclemlopn  13329  limcimolemlt  13348  cnplimcim  13351  cnplimclemr  13353  limccnp2lem  13360  limccnp2cntop  13361  dvfvalap  13365  dvconst  13376  dvaddxxbr  13380  dvmulxxbr  13381  dvcjbr  13387  dvexp  13390  dvrecap  13392  dvmptclx  13395  dvmptaddx  13396  dvmptmulx  13397  dvmptcmulcn  13398  dveflem  13402  dvef  13403  reeff1oleme  13408  sin0pilem1  13417  sin0pilem2  13418  efper  13443  sinperlem  13444  sinmpi  13451  cosmpi  13452  sinppi  13453  cosppi  13454  efimpi  13455  ptolemy  13460  sinq12gt0  13466  coseq0negpitopi  13472  tangtx  13474  abssinper  13482  cosq34lt1  13486  relogexp  13508  logdivlti  13517  logcxp  13533  rpcxp0  13534  rpcxp1  13535  1cxp  13536  ecxp  13537  rpcxpadd  13541  rpcxpp1  13542  rpmulcxp  13545  rpdivcxp  13547  cxpmul  13548  rpcxproot  13549  abscxp  13550  rpcxpsqrtth  13565  rplogbid1  13580  rplogb1  13581  rpelogb  13582  rplogbreexp  13586  rplogbzexp  13587  rprelogbmul  13588  rprelogbmulexp  13589  rprelogbdiv  13590  logbrec  13593  rpcxplogb  13597  logbgcd1irr  13600  logbgcd1irraplemexp  13601  logbgcd1irraplemap  13602  binom4  13612  lgslem1  13616  lgsval2lem  13626  lgsvalmod  13635  lgsneg  13640  lgsdir2lem4  13647  lgsdirprm  13650  lgsdir  13651  lgsdilem2  13652  lgsdi  13653  lgsne0  13654  lgsmodeq  13661  lgsdirnn0  13663  lgsdinn0  13664  2sqlem3  13668  2sqlem4  13669  2sqlem8  13674  djucllem  13756  bj-charfun  13764  bj-charfundc  13765  bj-charfundcALT  13766  nninfsellemeq  13969  nninffeq  13975  qdencn  13981  cvgcmp2nlemabs  13986  trilpolemisumle  13992  trilpolemeq1  13994  trilpolemlt1  13995  apdifflemf  14000  redcwlpolemeq1  14008  dceqnconst  14013  dcapnconst  14014  nconstwlpolem0  14016  nconstwlpolemgt0  14017  nconstwlpolem  14018