Theorem eqtrd 2187

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 2166	. 2 |- ( ph -> ( A = B <-> A = C ) )
4	1, 3	mpbid 146	1 |- ( ph -> A = C )

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 1487  ax-17 1503  ax-ext 2136

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

This theorem is referenced by:  eqtr2d  2188  eqtr3d  2189  eqtr4d  2190  3eqtrd  2191  3eqtrrd  2192  3eqtr2d  2193  syl5eq  2199  eqtrdi  2203  rabeqbidv  2704  rabeqbidva  2705  csbidmg  3083  csbco3g  3085  difeq12d  3222  ifeq12d  3520  ifbieq1d  3523  ifbieq2d  3525  ifbieq12d  3527  eqifdc  3535  csbsng  3616  disjpr2  3619  csbunig  3776  iuneq12d  3869  unisn3  4399  op1stbg  4433  opthreg  4509  onsucuni2  4517  csbxpg  4660  coeq12d  4743  csbdmg  4773  reseq12d  4860  csbresg  4862  resima2  4893  imaeq12d  4922  csbrng  5040  opswapg  5065  relcnvtr  5098  relcoi2  5109  relcoi1  5110  iotaint  5141  funprg  5213  funtpg  5214  funcnvres2  5238  fnco  5271  fococnv2  5433  fveq12d  5468  csbfv12g  5497  csbfv2g  5498  csbfvg  5499  dffn5im  5507  funfvdm2  5525  fvun1  5527  fvmpt2d  5547  fvmptt  5552  fndmin  5567  fniniseg2  5582  fnniniseg2  5583  fmptcof  5627  fvresi  5653  fvunsng  5654  fvpr1g  5666  fvpr2g  5667  fvtp1g  5668  funiunfvdm  5704  fcof1o  5730  riotaeqbidv  5773  oveq123d  5835  csbov12g  5850  csbov1g  5851  csbov2g  5852  ovmpodxf  5936  caov42d  5997  caovdilemd  6002  caovimo  6004  grprinvd  6006  offeq  6035  offval2  6037  caofinvl  6044  ot1stg  6090  ot2ndg  6091  2nd1st  6118  mpomptsx  6135  dmmpossx  6137  fmpox  6138  fmpoco  6153  1stconst  6158  algrflemg  6167  tfrexlem  6271  rdgivallem  6318  rdgisuc1  6321  frec0g  6334  frecabcl  6336  frecsuclem  6343  frecrdg  6345  oa0  6393  oasuc  6400  oa1suc  6403  omsuc  6408  nnaass  6421  nndi  6422  nnmass  6423  nnm2  6461  nn2m  6462  ereq1  6476  errn  6491  uniqs2  6529  oviec  6575  ecovass  6578  ecoviass  6579  ecovdi  6580  ecovidi  6581  mapsnconst  6628  mapen  6780  mapxpen  6782  xpmapenlem  6783  phplem4on  6801  fidifsnen  6804  undifdc  6857  fiintim  6862  fisseneq  6865  snexxph  6883  sbthlemi4  6893  sbthlemi6  6895  supeq2  6921  eqsupti  6928  infvalti  6954  djuf1olem  6983  djuss  7000  1stinl  7004  2ndinl  7005  1stinr  7006  2ndinr  7007  updjudhcoinlf  7010  updjudhcoinrg  7011  omp1eomlem  7024  difinfsn  7030  ctmlemr  7038  ctssdclemn0  7040  ctssdc  7043  enumctlemm  7044  enwomnilem  7091  en2other2  7110  cc3  7167  mulidpi  7217  addasspig  7229  mulasspig  7231  distrpig  7232  indpi  7241  addcmpblnq  7266  mulpipq  7271  dmaddpqlem  7276  nqpi  7277  addcomnqg  7280  recrecnq  7293  ltsonq  7297  ltanqg  7299  ltmnqg  7300  ltaddnq  7306  ltexnqq  7307  archnqq  7316  prarloclemarch  7317  ltrnqg  7319  ltnnnq  7322  nq0nn  7341  addcmpblnq0  7342  nqpnq0nq  7352  nqnq0a  7353  nq0m0r  7355  nq0a0  7356  distrnq0  7358  addassnq0  7361  nq02m  7364  prarloclemlo  7393  prarloclemcalc  7401  addnqprllem  7426  addnqprulem  7427  addnqprl  7428  addnqpru  7429  appdivnq  7462  mulnqprl  7467  mulnqpru  7468  addcanprlemu  7514  ltaprlem  7517  ltmprr  7541  cauappcvgprlemladdrl  7556  mulcmpblnrlemg  7639  mulcomsrg  7656  distrsrg  7658  ltsosr  7663  1idsr  7667  00sr  7668  ltasrg  7669  recexgt0sr  7672  srpospr  7682  prsradd  7685  prsrriota  7687  caucvgsrlemcau  7692  caucvgsrlemgt1  7694  caucvgsrlemoffval  7695  caucvgsrlemoffres  7699  caucvgsr  7701  map2psrprg  7704  elreal2  7729  mulresr  7737  pitonnlem1p1  7745  pitonnlem2  7746  pitoregt0  7748  recidpirqlemcalc  7756  recidpirq  7757  axaddcl  7763  axmulcl  7765  axmulcom  7770  axmulass  7772  axdistr  7773  ax1rid  7776  axcnre  7780  recriota  7789  axcaucvglemcau  7797  mulid1  7854  mulid2  7855  adddirp1d  7883  joinlmuladdmuld  7884  muladd11  7987  1p1times  7988  readdcan  7994  comraddd  8011  add42  8016  npcan  8063  addsubass  8064  2addsub  8068  addsubeq4  8069  nppcan  8076  nnpcan  8077  npncan2  8081  nncan  8083  subsub  8084  nnncan  8089  nnncan1  8090  pnpcan2  8094  pnncan  8095  subneg  8103  negneg  8104  negdi2  8112  mvrraddd  8220  assraddsubd  8222  subaddeqd  8223  addid0  8227  mul02  8241  mul01  8243  mulneg1  8249  mul2neg  8252  mulm1  8254  ltadd2  8273  rimul  8439  rereim  8440  mulreim  8458  recextlem1  8504  mulcanapd  8514  divcanap1  8533  divrecap2  8541  divmulassap  8547  divmulasscomap  8548  divcanap4  8551  dividap  8553  muldivdirap  8559  divdivdivap  8565  recdivap  8570  divadddivap  8579  divsubdivap  8580  div2negap  8587  divcanap5rd  8670  dmdcanap2d  8673  subrecap  8690  recgt0  8700  lt2mul2div  8729  nnmulcl  8833  times2  8941  add1p1  9061  sub1m1  9062  cnm2m1cnm3  9063  nn0supp  9121  peano2z  9182  nneoor  9245  supminfex  9487  cnref1o  9537  rexneg  9712  xaddpnf1  9728  xaddmnf1  9730  rexadd  9734  xaddid1  9744  xaddid2  9745  xaddass  9751  xpncan  9753  xleadd1a  9755  xltadd1  9758  xposdif  9764  xadd4d  9767  xleaddadd  9769  iooidg  9791  iooval2  9797  icoshftf1o  9873  lincmb01cmp  9885  iccf1o  9886  fzval2  9893  fzsuc  9949  fzpred  9950  fztpval  9963  fseq1p1m1  9974  fzshftral  9988  fzo0to3tp  10096  fzo0sn0fzo1  10098  fzosplitsn  10110  fzosplitprm1  10111  fzisfzounsn  10113  rebtwn2zlemstep  10130  2tnp1ge0ge0  10178  flqdiv  10198  modqvalr  10202  modqdiffl  10212  modqfrac  10214  modqmulnn  10219  modqid  10226  modqcyc  10236  modqcyc2  10237  mulp1mod1  10242  modqmuladd  10243  modqmuladdnn0  10245  qnegmod  10246  m1modnnsub1  10247  addmodid  10249  addmodidr  10250  modqmul12d  10255  modqnegd  10256  modqadd12d  10257  modifeq2int  10263  modqaddmulmod  10268  modqdi  10269  modqsubdir  10270  modsumfzodifsn  10273  addmodlteq  10275  frec2uzsucd  10278  frecuzrdgrrn  10285  frec2uzrdg  10286  frecuzrdglem  10288  frecuzrdgsuc  10291  frecuzrdgg  10293  frecuzrdgdomlem  10294  frecuzrdgfunlem  10296  frecuzrdgtclt  10298  frecuzrdgsuctlem  10300  frecfzennn  10303  seqeq1  10325  seq3val  10335  seqvalcd  10336  seq3p1  10339  seqp1cd  10343  seq3feq2  10347  seq3fveq  10348  seq3shft2  10350  seq3-1p  10357  iseqf1olemnab  10365  iseqf1olemab  10366  iseqf1olemnanb  10367  iseqf1olemqk  10371  iseqf1olemfvp  10374  seq3f1olemqsumkj  10375  seq3f1olemqsumk  10376  seq3f1olemqsum  10377  seq3f1o  10381  seq3id3  10384  seq3z  10388  fser0const  10393  exp3vallem  10398  expnnval  10400  expp1  10404  expn1ap0  10407  mulexp  10436  expaddzaplem  10440  expaddzap  10441  expmul  10442  expp1zap  10446  expm1ap  10447  sqval  10455  iexpcyc  10501  subsq2  10504  binom2  10507  binom21  10508  binom2sub1  10510  mulbinom2  10512  binom3  10513  zesq  10514  bernneq  10516  sqoddm1div8  10548  nn0opthlem1d  10571  facp1  10581  faclbnd6  10595  bcval2  10601  bcval3  10602  bcn0  10606  bcp1n  10612  bcp1nk  10613  bcn2  10615  bcp1m1  10616  bcpasc  10617  bcn2m1  10620  hashinfom  10629  hashennn  10631  hashfz1  10634  fseq1hash  10652  omgadd  10653  hashunsng  10658  hashprg  10659  hashdifsn  10670  hashdifpr  10671  hashfz  10672  hashfzo  10673  hashfzo0  10674  hashfzp1  10675  hashfz0  10676  hashxp  10677  resunimafz0  10679  fnfz0hash  10680  ffzo0hash  10682  hashfacen  10684  zfz1isolemsplit  10686  zfz1isolemiso  10687  zfz1isolem1  10688  shftdm  10699  shftval2  10703  shftval4  10705  shftval5  10706  shftcan1  10711  seq3shft  10715  imre  10728  crre  10734  remim  10737  reim0b  10739  recj  10744  reneg  10745  readd  10746  resub  10747  remullem  10748  imcj  10752  imneg  10753  imadd  10754  imsub  10755  cjcj  10760  cjadd  10761  ipcnval  10763  cjneg  10767  cjsub  10769  cjexp  10770  imval2  10771  cjap  10783  resqrexlemf1  10885  resqrexlemfp1  10886  resqrexlemover  10887  resqrexlemcalc1  10891  resqrexlemcalc3  10893  resqrexlemnm  10895  resqrexlemcvg  10896  resqrtcl  10906  sqrtsq  10921  absneg  10927  absvalsq  10930  absvalsq2  10931  sqabsadd  10932  sqabssub  10933  absval2  10934  absreimsq  10944  absmul  10946  absexp  10956  absexpzap  10957  abssuble0  10980  abstri  10981  recan  10986  amgm2  10995  maxabslemlub  11084  max0addsup  11096  minmax  11106  minabs  11112  bdtrilem  11115  bdtri  11116  xrmaxiflemab  11121  xrmaxiflemcom  11123  xrmaxadd  11135  xrminmax  11139  xrmineqinf  11143  xrminrecl  11147  xrbdtri  11150  climshft2  11180  subcn2  11185  reccn2ap  11187  climaddc2  11204  iser3shft  11220  climcvg1nlem  11223  sumeq12dv  11246  sumeq12rdv  11247  sumrbdclem  11251  fsum3cvg  11252  summodclem3  11254  summodclem2a  11255  summodc  11257  fsum3  11261  isumz  11263  fsumf1o  11264  fisumss  11266  fsumsersdc  11269  fsum3ser  11271  fsumsplit  11281  fsumsplitf  11282  sumsnf  11283  fsumsplitsn  11284  fsum1  11286  sumpr  11287  sumtp  11288  fsumm1  11290  fsum1p  11292  fsumsplitsnun  11293  fsump1  11294  isumclim  11295  sumnul  11298  isumadd  11305  fsum2dlemstep  11308  fsumcnv  11311  fisumcom2  11312  fsumshftm  11319  fisumrev2  11320  fisum0diag2  11321  fsumsub  11326  fsumdifsnconst  11329  modfsummodlemstep  11331  fsumabs  11339  telfsumo  11340  telfsum  11342  telfsum2  11343  fsumparts  11344  fsumiun  11351  hashiun  11352  hash2iun  11353  hash2iun1dif1  11354  binomlem  11357  binom1p  11359  binom11  11360  binom1dif  11361  bcxmas  11363  isum1p  11366  isumnn0nn  11367  isumlessdc  11370  divcnv  11371  arisum2  11373  trireciplem  11374  geosergap  11380  geolim  11385  georeclim  11387  geo2lim  11390  geoisum1  11393  cvgratnnlemnexp  11398  cvgratnnlemmn  11399  cvgratnnlemsumlt  11402  cvgratz  11406  mertenslemi1  11409  mertenslem2  11410  mertensabs  11411  prodfrecap  11420  prodeq12dv  11443  prodeq12rdv  11444  prodrbdclem  11445  fproddccvg  11446  prodmodclem3  11449  prodmodclem2a  11450  zprodap0  11455  fprodseq  11457  fprodntrivap  11458  prod1dc  11460  fprodf1o  11462  prodssdc  11463  fprodssdc  11464  prodsnf  11466  fprod1  11468  fprodsplitdc  11470  fprodm1  11472  fprod1p  11473  fprodp1  11474  fprodunsn  11478  fprodcl2lem  11479  fprodabs  11490  fprodconst  11494  fprod2dlemstep  11496  fprodcnv  11499  fprodcom2fi  11500  fprodrec  11503  fprodsplitsn  11507  fprodsplit1f  11508  fprodeq0g  11512  eftabs  11530  efcllemp  11532  ef0lem  11534  efcvgfsum  11541  ege2le3  11545  efcj  11547  efaddlem  11548  efexp  11556  eftlub  11564  efsep  11565  effsumlt  11566  ef4p  11568  efgt1p2  11569  efgt1p  11570  tanval2ap  11587  tanval3ap  11588  resinval  11589  recosval  11590  efi4p  11591  resin4p  11592  recos4p  11593  sinneg  11600  cosneg  11601  tannegap  11602  efmival  11607  sinadd  11610  cosadd  11611  tanaddaplem  11612  tanaddap  11613  sinsub  11614  cossub  11615  addsin  11616  subsin  11617  subcos  11621  sincossq  11622  sin2t  11623  sin01bnd  11631  cos01bnd  11632  absefi  11642  absef  11643  absefib  11644  efieq1re  11645  demoivre  11646  demoivreALT  11647  eirraplem  11650  dvdstr  11697  dvdsadd2b  11707  mulmoddvds  11728  ltoddhalfle  11757  opoe  11759  m1expo  11764  m1exp1  11765  flodddiv4  11798  flodddiv4t2lthalf  11801  zsupcllemstep  11805  nn0gcdid0  11837  gcdaddm  11840  gcdadd  11841  gcdid  11842  gcdabs  11844  modgcd  11847  1gcd  11848  bezout  11867  dfgcd2  11870  mulgcd  11872  absmulgcd  11873  gcdmultiple  11876  gcdmultiplez  11877  rpmulgcd  11882  rplpwr  11883  rppwr  11884  dvdssqlem  11886  ialgr0  11893  alginv  11896  algcvg  11897  algfx  11901  eucalginv  11905  eucalglt  11906  lcmcl  11921  lcmabs  11925  lcmgcdlem  11926  lcmdvds  11928  lcmgcdnn  11931  coprmdvds  11941  qredeq  11945  divgcdcoprm0  11950  divgcdcoprmex  11951  rpexp1i  12000  sqrt2irrlem  12007  sqpweven  12021  2sqpwodd  12022  sqrt2irraplemnn  12025  qmuldeneqnum  12041  nn0gcdsq  12046  numdensq  12048  nn0sqrtelqelz  12052  phibndlem  12060  dfphi2  12064  phiprmpw  12066  phiprm  12067  phimullem  12069  eulerthlem1  12071  eulerthlemh  12075  eulerthlemth  12076  eulerth  12077  hashgcdlem  12078  ennnfonelemp1  12094  ennnfonelemhdmp1  12097  ennnfonelemss  12098  ennnfonelemkh  12100  ennnfonelemhf1o  12101  ennnfonelemhom  12103  ennnfonelemnn0  12110  ctinfomlemom  12115  setsvala  12168  fvsetsid  12171  setsresg  12175  setscom  12177  setsslid  12187  ressid2  12196  ressval2  12197  restid2  12307  ntrval  12457  clsval  12458  cldcls  12461  neival  12490  resttop  12517  restco  12521  restabs  12522  resttopon2  12525  cnpval  12545  cnntr  12572  cnrest2  12583  upxp  12619  uptx  12621  cnmpt11  12630  cnmpt21  12638  psmetsym  12676  psmetres2  12680  xmetsym  12715  xmettxlem  12856  txmetcnp  12865  cnbl0  12881  cnblcld  12882  remetdval  12886  bl2ioo  12889  tgioo  12893  addcncntoplem  12898  divcnap  12902  fsumcncntop  12903  cncfmet  12926  cncfmptc  12929  addccncf  12933  negcncf  12935  mulcncflem  12937  ivthinclemlopn  12961  limcimolemlt  12980  cnplimcim  12983  cnplimclemr  12985  limccnp2lem  12992  limccnp2cntop  12993  dvfvalap  12997  dvconst  13008  dvaddxxbr  13012  dvmulxxbr  13013  dvcjbr  13019  dvexp  13022  dvrecap  13024  dvmptclx  13027  dvmptaddx  13028  dvmptmulx  13029  dvmptcmulcn  13030  dveflem  13034  dvef  13035  reeff1oleme  13040  sin0pilem1  13049  sin0pilem2  13050  efper  13075  sinperlem  13076  sinmpi  13083  cosmpi  13084  sinppi  13085  cosppi  13086  efimpi  13087  ptolemy  13092  sinq12gt0  13098  coseq0negpitopi  13104  tangtx  13106  abssinper  13114  cosq34lt1  13118  relogexp  13140  logdivlti  13149  logcxp  13165  rpcxp0  13166  rpcxp1  13167  1cxp  13168  ecxp  13169  rpcxpadd  13173  rpcxpp1  13174  rpmulcxp  13177  rpdivcxp  13179  cxpmul  13180  rpcxproot  13181  abscxp  13182  rpcxpsqrtth  13197  rplogbid1  13211  rplogb1  13212  rpelogb  13213  rplogbreexp  13217  rplogbzexp  13218  rprelogbmul  13219  rprelogbmulexp  13220  rprelogbdiv  13221  logbrec  13224  rpcxplogb  13228  logbgcd1irr  13231  logbgcd1irraplemexp  13232  logbgcd1irraplemap  13233  djucllem  13320  bj-charfun  13328  bj-charfundc  13329  bj-charfundcALT  13330  nninfalllemn  13528  nninfsellemeq  13535  nninffeq  13541  qdencn  13547  cvgcmp2nlemabs  13552  trilpolemisumle  13558  trilpolemeq1  13560  trilpolemlt1  13561  apdifflemf  13566  redcwlpolemeq1  13574  dceqnconst  13579  dcapnconst  13580  nconstwlpolem0  13582  nconstwlpolemgt0  13583  nconstwlpolem  13584