Theorem eqtrd 2210

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrd.1	|- ( ph -> A = B )
eqtrd.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtrd	|- ( ph -> A = C )

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 |- ( ph -> A = B )
2		eqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eqeq2d 2189	. 2 |- ( ph -> ( A = B <-> A = C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtr2d  2211  eqtr3d  2212  eqtr4d  2213  3eqtrd  2214  3eqtrrd  2215  3eqtr2d  2216  eqtrid  2222  eqtrdi  2226  rabeqbidv  2732  rabeqbidva  2733  csbidmg  3113  csbco3g  3115  difeq12d  3254  ifeq12d  3553  ifbieq1d  3556  ifbieq2d  3558  ifbieq12d  3560  eqifdc  3568  csbsng  3652  disjpr2  3655  csbunig  3815  iuneq12d  3908  unisn3  4442  op1stbg  4476  opthreg  4552  onsucuni2  4560  csbxpg  4704  coeq12d  4787  csbdmg  4817  reseq12d  4904  csbresg  4906  resima2  4937  imaeq12d  4967  csbrng  5086  opswapg  5111  relcnvtr  5144  relcoi2  5155  relcoi1  5156  iotaint  5187  funprg  5262  funtpg  5263  funcnvres2  5287  fnco  5320  fococnv2  5483  fveq12d  5518  csbfv12g  5547  csbfv2g  5548  csbfvg  5549  dffn5im  5557  funfvdm2  5576  fvun1  5578  fvmpt2d  5598  fvmptt  5603  fndmin  5619  fniniseg2  5634  fnniniseg2  5635  fmptcof  5679  fvresi  5705  fvunsng  5706  fvpr1g  5718  fvpr2g  5719  fvtp1g  5720  funiunfvdm  5758  fcof1o  5784  riotaeqbidv  5828  oveq123d  5890  csbov12g  5908  csbov1g  5909  csbov2g  5910  ovmpodxf  5994  caov42d  6055  caovdilemd  6060  caovimo  6062  offeq  6090  offval2  6092  caofinvl  6099  ot1stg  6147  ot2ndg  6148  2nd1st  6175  mpomptsx  6192  dmmpossx  6194  fmpox  6195  fmpoco  6211  1stconst  6216  algrflemg  6225  tfrexlem  6329  rdgivallem  6376  rdgisuc1  6379  frec0g  6392  frecabcl  6394  frecsuclem  6401  frecrdg  6403  oa0  6452  oasuc  6459  oa1suc  6462  omsuc  6467  nnaass  6480  nndi  6481  nnmass  6482  nnm2  6521  nn2m  6522  ereq1  6536  errn  6551  uniqs2  6589  oviec  6635  ecovass  6638  ecoviass  6639  ecovdi  6640  ecovidi  6641  mapsnconst  6688  mapen  6840  mapxpen  6842  xpmapenlem  6843  phplem4on  6861  fidifsnen  6864  undifdc  6917  fiintim  6922  fisseneq  6925  snexxph  6943  sbthlemi4  6953  sbthlemi6  6955  supeq2  6982  eqsupti  6989  infvalti  7015  djuf1olem  7046  djuss  7063  1stinl  7067  2ndinl  7068  1stinr  7069  2ndinr  7070  updjudhcoinlf  7073  updjudhcoinrg  7074  omp1eomlem  7087  difinfsn  7093  ctmlemr  7101  ctssdclemn0  7103  ctssdc  7106  enumctlemm  7107  nnnninfeq  7120  nnnninfeq2  7121  nninfisollemne  7123  nninfisol  7125  enwomnilem  7161  nninfwlpoimlemg  7167  nninfwlpoimlemginf  7168  en2other2  7189  cc3  7258  mulidpi  7308  addasspig  7320  mulasspig  7322  distrpig  7323  indpi  7332  addcmpblnq  7357  mulpipq  7362  dmaddpqlem  7367  nqpi  7368  addcomnqg  7371  recrecnq  7384  ltsonq  7388  ltanqg  7390  ltmnqg  7391  ltaddnq  7397  ltexnqq  7398  archnqq  7407  prarloclemarch  7408  ltrnqg  7410  ltnnnq  7413  nq0nn  7432  addcmpblnq0  7433  nqpnq0nq  7443  nqnq0a  7444  nq0m0r  7446  nq0a0  7447  distrnq0  7449  addassnq0  7452  nq02m  7455  prarloclemlo  7484  prarloclemcalc  7492  addnqprllem  7517  addnqprulem  7518  addnqprl  7519  addnqpru  7520  appdivnq  7553  mulnqprl  7558  mulnqpru  7559  addcanprlemu  7605  ltaprlem  7608  ltmprr  7632  cauappcvgprlemladdrl  7647  mulcmpblnrlemg  7730  mulcomsrg  7747  distrsrg  7749  ltsosr  7754  1idsr  7758  00sr  7759  ltasrg  7760  recexgt0sr  7763  srpospr  7773  prsradd  7776  prsrriota  7778  caucvgsrlemcau  7783  caucvgsrlemgt1  7785  caucvgsrlemoffval  7786  caucvgsrlemoffres  7790  caucvgsr  7792  map2psrprg  7795  elreal2  7820  mulresr  7828  pitonnlem1p1  7836  pitonnlem2  7837  pitoregt0  7839  recidpirqlemcalc  7847  recidpirq  7848  axaddcl  7854  axmulcl  7856  axmulcom  7861  axmulass  7863  axdistr  7864  ax1rid  7867  axcnre  7871  recriota  7880  axcaucvglemcau  7888  mulid1  7945  mulid2  7946  adddirp1d  7974  joinlmuladdmuld  7975  muladd11  8080  1p1times  8081  readdcan  8087  comraddd  8104  add42  8109  npcan  8156  addsubass  8157  2addsub  8161  addsubeq4  8162  nppcan  8169  nnpcan  8170  npncan2  8174  nncan  8176  subsub  8177  nnncan  8182  nnncan1  8183  pnpcan2  8187  pnncan  8188  subneg  8196  negneg  8197  negdi2  8205  mvrraddd  8313  assraddsubd  8315  subaddeqd  8316  addid0  8320  mul02  8334  mul01  8336  mulneg1  8342  mul2neg  8345  mulm1  8347  ltadd2  8366  rimul  8532  rereim  8533  mulreim  8551  recextlem1  8597  mulcanapd  8607  divcanap1  8627  divrecap2  8635  divmulassap  8641  divmulasscomap  8642  divcanap4  8645  dividap  8647  muldivdirap  8653  divdivdivap  8659  recdivap  8664  divadddivap  8673  divsubdivap  8674  div2negap  8681  divcanap5rd  8764  dmdcanap2d  8767  subrecap  8785  recgt0  8796  lt2mul2div  8825  nnmulcl  8929  times2  9037  add1p1  9157  sub1m1  9158  cnm2m1cnm3  9159  nn0supp  9217  peano2z  9278  nneoor  9344  supminfex  9586  cnref1o  9639  rexneg  9817  xaddpnf1  9833  xaddmnf1  9835  rexadd  9839  xaddid1  9849  xaddid2  9850  xaddass  9856  xpncan  9858  xleadd1a  9860  xltadd1  9863  xposdif  9869  xadd4d  9872  xleaddadd  9874  iooidg  9896  iooval2  9902  icoshftf1o  9978  lincmb01cmp  9990  iccf1o  9991  fzval2  9998  fzsuc  10055  fzpred  10056  fztpval  10069  fseq1p1m1  10080  fzshftral  10094  fz0to4untppr  10110  fzo0to3tp  10205  fzo0sn0fzo1  10207  fzosplitsn  10219  fzosplitprm1  10220  fzisfzounsn  10222  rebtwn2zlemstep  10239  2tnp1ge0ge0  10287  flqdiv  10307  modqvalr  10311  modqdiffl  10321  modqfrac  10323  modqmulnn  10328  modqid  10335  modqcyc  10345  modqcyc2  10346  mulp1mod1  10351  modqmuladd  10352  modqmuladdnn0  10354  qnegmod  10355  m1modnnsub1  10356  addmodid  10358  addmodidr  10359  modqmul12d  10364  modqnegd  10365  modqadd12d  10366  modifeq2int  10372  modqaddmulmod  10377  modqdi  10378  modqsubdir  10379  modsumfzodifsn  10382  addmodlteq  10384  frec2uzsucd  10387  frecuzrdgrrn  10394  frec2uzrdg  10395  frecuzrdglem  10397  frecuzrdgsuc  10400  frecuzrdgg  10402  frecuzrdgdomlem  10403  frecuzrdgfunlem  10405  frecuzrdgtclt  10407  frecuzrdgsuctlem  10409  frecfzennn  10412  seqeq1  10434  seq3val  10444  seqvalcd  10445  seq3p1  10448  seqp1cd  10452  seq3feq2  10456  seq3fveq  10457  seq3shft2  10459  seq3-1p  10466  iseqf1olemnab  10474  iseqf1olemab  10475  iseqf1olemnanb  10476  iseqf1olemqk  10480  iseqf1olemfvp  10483  seq3f1olemqsumkj  10484  seq3f1olemqsumk  10485  seq3f1olemqsum  10486  seq3f1o  10490  seq3id3  10493  seq3z  10497  fser0const  10502  exp3vallem  10507  expnnval  10509  expp1  10513  expn1ap0  10516  mulexp  10545  expaddzaplem  10549  expaddzap  10550  expmul  10551  expp1zap  10555  expm1ap  10556  sqval  10564  iexpcyc  10610  subsq2  10613  qsqeqor  10616  binom2  10617  binom21  10618  binom2sub1  10620  mulbinom2  10622  binom3  10623  zesq  10624  bernneq  10626  sqoddm1div8  10659  nn0opthlem1d  10684  facp1  10694  faclbnd6  10708  bcval2  10714  bcval3  10715  bcn0  10719  bcp1n  10725  bcp1nk  10726  bcn2  10728  bcp1m1  10729  bcpasc  10730  bcn2m1  10733  hashinfom  10742  hashennn  10744  hashfz1  10747  fseq1hash  10765  omgadd  10766  hashunsng  10771  hashprg  10772  hashdifsn  10783  hashdifpr  10784  hashfz  10785  hashfzo  10786  hashfzo0  10787  hashfzp1  10788  hashfz0  10789  hashxp  10790  resunimafz0  10795  fnfz0hash  10796  ffzo0hash  10798  hashfacen  10800  zfz1isolemsplit  10802  zfz1isolemiso  10803  zfz1isolem1  10804  shftdm  10815  shftval2  10819  shftval4  10821  shftval5  10822  shftcan1  10827  seq3shft  10831  imre  10844  crre  10850  remim  10853  reim0b  10855  recj  10860  reneg  10861  readd  10862  resub  10863  remullem  10864  imcj  10868  imneg  10869  imadd  10870  imsub  10871  cjcj  10876  cjadd  10877  ipcnval  10879  cjneg  10883  cjsub  10885  cjexp  10886  imval2  10887  cjap  10899  resqrexlemf1  11001  resqrexlemfp1  11002  resqrexlemover  11003  resqrexlemcalc1  11007  resqrexlemcalc3  11009  resqrexlemnm  11011  resqrexlemcvg  11012  resqrtcl  11022  sqrtsq  11037  absneg  11043  absvalsq  11046  absvalsq2  11047  sqabsadd  11048  sqabssub  11049  absval2  11050  absreimsq  11060  absmul  11062  absexp  11072  absexpzap  11073  abssuble0  11096  abstri  11097  recan  11102  amgm2  11111  maxabslemlub  11200  max0addsup  11212  minmax  11222  minabs  11228  bdtrilem  11231  bdtri  11232  xrmaxiflemab  11239  xrmaxiflemcom  11241  xrmaxadd  11253  xrminmax  11257  xrmineqinf  11261  xrminrecl  11265  xrbdtri  11268  climshft2  11298  subcn2  11303  reccn2ap  11305  climaddc2  11322  iser3shft  11338  climcvg1nlem  11341  sumeq12dv  11364  sumeq12rdv  11365  sumrbdclem  11369  fsum3cvg  11370  summodclem3  11372  summodclem2a  11373  summodc  11375  fsum3  11379  isumz  11381  fsumf1o  11382  fisumss  11384  fsumsersdc  11387  fsum3ser  11389  fsumsplit  11399  fsumsplitf  11400  sumsnf  11401  fsumsplitsn  11402  fsum1  11404  sumpr  11405  sumtp  11406  fsumm1  11408  fsum1p  11410  fsumsplitsnun  11411  fsump1  11412  isumclim  11413  sumnul  11416  isumadd  11423  fsum2dlemstep  11426  fsumcnv  11429  fisumcom2  11430  fsumshftm  11437  fisumrev2  11438  fisum0diag2  11439  fsumsub  11444  fsumdifsnconst  11447  modfsummodlemstep  11449  fsumabs  11457  telfsumo  11458  telfsum  11460  telfsum2  11461  fsumparts  11462  fsumiun  11469  hashiun  11470  hash2iun  11471  hash2iun1dif1  11472  binomlem  11475  binom1p  11477  binom11  11478  binom1dif  11479  bcxmas  11481  isum1p  11484  isumnn0nn  11485  isumlessdc  11488  divcnv  11489  arisum2  11491  trireciplem  11492  geosergap  11498  geolim  11503  georeclim  11505  geo2lim  11508  geoisum1  11511  cvgratnnlemnexp  11516  cvgratnnlemmn  11517  cvgratnnlemsumlt  11520  cvgratz  11524  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  prodfrecap  11538  prodeq12dv  11561  prodeq12rdv  11562  prodrbdclem  11563  fproddccvg  11564  prodmodclem3  11567  prodmodclem2a  11568  zprodap0  11573  fprodseq  11575  fprodntrivap  11576  prod1dc  11578  fprodf1o  11580  prodssdc  11581  fprodssdc  11582  prodsnf  11584  fprod1  11586  fprodsplitdc  11588  fprodm1  11590  fprod1p  11591  fprodp1  11592  fprodunsn  11596  fprodcl2lem  11597  fprodabs  11608  fprodconst  11612  fprod2dlemstep  11614  fprodcnv  11617  fprodcom2fi  11618  fprodrec  11621  fprodsplitsn  11625  fprodsplit1f  11626  fprodeq0g  11630  eftabs  11648  efcllemp  11650  ef0lem  11652  efcvgfsum  11659  ege2le3  11663  efcj  11665  efaddlem  11666  efexp  11674  eftlub  11682  efsep  11683  effsumlt  11684  ef4p  11686  efgt1p2  11687  efgt1p  11688  tanval2ap  11705  tanval3ap  11706  resinval  11707  recosval  11708  efi4p  11709  resin4p  11710  recos4p  11711  sinneg  11718  cosneg  11719  tannegap  11720  efmival  11725  sinadd  11728  cosadd  11729  tanaddaplem  11730  tanaddap  11731  sinsub  11732  cossub  11733  addsin  11734  subsin  11735  subcos  11739  sincossq  11740  sin2t  11741  sin01bnd  11749  cos01bnd  11750  absefi  11760  absef  11761  absefib  11762  efieq1re  11763  demoivre  11764  demoivreALT  11765  eirraplem  11768  dvdstr  11819  dvdsadd2b  11831  mulmoddvds  11852  ltoddhalfle  11881  opoe  11883  m1expo  11888  m1exp1  11889  flodddiv4  11922  flodddiv4t2lthalf  11925  zsupcllemstep  11929  nn0gcdid0  11965  gcdaddm  11968  gcdadd  11969  gcdid  11970  gcdabs  11972  modgcd  11975  1gcd  11976  bezout  11995  dfgcd2  11998  mulgcd  12000  absmulgcd  12001  gcdmultiple  12004  gcdmultiplez  12005  rpmulgcd  12010  rplpwr  12011  rppwr  12012  dvdssqlem  12014  uzwodc  12021  ialgr0  12027  alginv  12030  algcvg  12031  algfx  12035  eucalginv  12039  eucalglt  12040  lcmcl  12055  lcmabs  12059  lcmgcdlem  12060  lcmdvds  12062  lcmgcdnn  12065  coprmdvds  12075  qredeq  12079  divgcdcoprm0  12084  divgcdcoprmex  12085  rpexp1i  12137  sqrt2irrlem  12144  sqpweven  12158  2sqpwodd  12159  sqrt2irraplemnn  12162  qmuldeneqnum  12178  nn0gcdsq  12183  numdensq  12185  nn0sqrtelqelz  12189  phibndlem  12199  dfphi2  12203  phiprmpw  12205  phiprm  12206  phimullem  12208  eulerthlem1  12210  eulerthlemh  12214  eulerthlemth  12215  eulerth  12216  prmdiv  12218  hashgcdlem  12221  phisum  12223  odzdvds  12228  vfermltl  12234  powm2modprm  12235  modprm0  12237  nnnn0modprm0  12238  coprimeprodsq  12240  pythagtriplem1  12248  pythagtriplem3  12250  pythagtriplem4  12251  pythagtriplem6  12253  pythagtriplem7  12254  pythagtriplem14  12260  pythagtriplem16  12262  pceulem  12277  pcval  12279  pczpre  12280  pcdiv  12285  pc1  12288  pcrec  12291  pcexp  12292  pcid  12306  pcneg  12307  pcgcd1  12310  pc2dvds  12312  difsqpwdvds  12320  pcaddlem  12321  pcadd  12322  pcmpt  12324  pcmpt2  12325  pcprod  12327  pcfac  12331  prmpwdvds  12336  pockthlem  12337  1arithlem2  12345  4sqlem9  12367  4sqlem4  12373  mul4sqlem  12374  ennnfonelemp1  12390  ennnfonelemhdmp1  12393  ennnfonelemss  12394  ennnfonelemkh  12396  ennnfonelemhf1o  12397  ennnfonelemhom  12399  ennnfonelemnn0  12406  ctinfomlemom  12411  setsvala  12476  fvsetsid  12479  setsresg  12483  setscom  12485  setsslid  12495  ressbasd  12509  ressabsg  12517  restid2  12645  lidrididd  12693  grprinvd  12697  mndpropd  12733  mhmf1o  12751  mhmco  12764  grpinvval  12806  isgrpinv  12816  grpsubinv  12832  grpidssd  12835  grpinvsub  12841  grpsubid  12843  grpsubadd0sub  12846  grpsubsub  12848  grpnpncan0  12855  grpnnncan2  12856  grpsubpropd2  12864  grp1inv  12866  ghmgrp  12871  mulgnn  12878  mulgnnp1  12880  mulg2  12881  mulgnegnn  12882  mulgneg  12890  mulgnegneg  12891  mulgm1  12892  mulgaddcom  12895  mulginvcom  12896  mulgnn0z  12898  mulgz  12899  mulgnn0dir  12901  mulgdirlem  12902  mulgp1  12904  mulgnnass  12906  mulgnn0ass  12907  mulgass  12908  mulgassr  12909  mhmmulg  12912  mulgpropdg  12913  rinvmod  12939  ablsub4  12943  ablpncan3  12947  ablnnncan  12953  ablnnncan1  12954  mgptopng  12966  srgass  12980  srgmulgass  12998  srgpcomp  12999  srgpcomppsc  13001  srglmhm  13002  srgrmhm  13003  ringcom  13040  ringpropd  13043  crngpropd  13044  isringd  13046  iscrngd  13047  ringinvnzdiv  13053  ringnegl  13054  rngnegr  13055  ringsubdi  13059  rngsubdir  13060  mulgass2  13061  opprmulg  13068  opprring  13074  oppr1g  13077  isunitd  13100  unitmulcl  13107  unitgrp  13110  invrfvald  13116  dvrid  13131  dvrcan1  13134  rngidpropdg  13138  unitpropdg  13140  invrpropdg  13141  ntrval  13277  clsval  13278  cldcls  13281  neival  13310  resttop  13337  restco  13341  restabs  13342  resttopon2  13345  cnpval  13365  cnntr  13392  cnrest2  13403  upxp  13439  uptx  13441  cnmpt11  13450  cnmpt21  13458  psmetsym  13496  psmetres2  13500  xmetsym  13535  xmettxlem  13676  txmetcnp  13685  cnbl0  13701  cnblcld  13702  remetdval  13706  bl2ioo  13709  tgioo  13713  addcncntoplem  13718  divcnap  13722  fsumcncntop  13723  cncfmet  13746  cncfmptc  13749  addccncf  13753  negcncf  13755  mulcncflem  13757  ivthinclemlopn  13781  limcimolemlt  13800  cnplimcim  13803  cnplimclemr  13805  limccnp2lem  13812  limccnp2cntop  13813  dvfvalap  13817  dvconst  13828  dvaddxxbr  13832  dvmulxxbr  13833  dvcjbr  13839  dvexp  13842  dvrecap  13844  dvmptclx  13847  dvmptaddx  13848  dvmptmulx  13849  dvmptcmulcn  13850  dveflem  13854  dvef  13855  reeff1oleme  13860  sin0pilem1  13869  sin0pilem2  13870  efper  13895  sinperlem  13896  sinmpi  13903  cosmpi  13904  sinppi  13905  cosppi  13906  efimpi  13907  ptolemy  13912  sinq12gt0  13918  coseq0negpitopi  13924  tangtx  13926  abssinper  13934  cosq34lt1  13938  relogexp  13960  logdivlti  13969  logcxp  13985  rpcxp0  13986  rpcxp1  13987  1cxp  13988  ecxp  13989  rpcxpadd  13993  rpcxpp1  13994  rpmulcxp  13997  rpdivcxp  13999  cxpmul  14000  rpcxproot  14001  abscxp  14002  rpcxpsqrtth  14017  rplogbid1  14032  rplogb1  14033  rpelogb  14034  rplogbreexp  14038  rplogbzexp  14039  rprelogbmul  14040  rprelogbmulexp  14041  rprelogbdiv  14042  logbrec  14045  rpcxplogb  14049  logbgcd1irr  14052  logbgcd1irraplemexp  14053  logbgcd1irraplemap  14054  binom4  14064  lgslem1  14068  lgsval2lem  14078  lgsvalmod  14087  lgsneg  14092  lgsdir2lem4  14099  lgsdirprm  14102  lgsdir  14103  lgsdilem2  14104  lgsdi  14105  lgsne0  14106  lgsmodeq  14113  lgsdirnn0  14115  lgsdinn0  14116  2sqlem3  14120  2sqlem4  14121  2sqlem8  14126  djucllem  14208  bj-charfun  14215  bj-charfundc  14216  bj-charfundcALT  14217  nninfsellemeq  14419  nninffeq  14425  qdencn  14431  cvgcmp2nlemabs  14436  trilpolemisumle  14442  trilpolemeq1  14444  trilpolemlt1  14445  apdifflemf  14450  redcwlpolemeq1  14458  dceqnconst  14463  dcapnconst  14464  nconstwlpolem0  14466  nconstwlpolemgt0  14467  nconstwlpolem  14468