Theorem eqtrd 2203

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

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  3545  ifbieq1d  3548  ifbieq2d  3550  ifbieq12d  3552  eqifdc  3560  csbsng  3644  disjpr2  3647  csbunig  3804  iuneq12d  3897  unisn3  4430  op1stbg  4464  opthreg  4540  onsucuni2  4548  csbxpg  4692  coeq12d  4775  csbdmg  4805  reseq12d  4892  csbresg  4894  resima2  4925  imaeq12d  4954  csbrng  5072  opswapg  5097  relcnvtr  5130  relcoi2  5141  relcoi1  5142  iotaint  5173  funprg  5248  funtpg  5249  funcnvres2  5273  fnco  5306  fococnv2  5468  fveq12d  5503  csbfv12g  5532  csbfv2g  5533  csbfvg  5534  dffn5im  5542  funfvdm2  5560  fvun1  5562  fvmpt2d  5582  fvmptt  5587  fndmin  5603  fniniseg2  5618  fnniniseg2  5619  fmptcof  5663  fvresi  5689  fvunsng  5690  fvpr1g  5702  fvpr2g  5703  fvtp1g  5704  funiunfvdm  5742  fcof1o  5768  riotaeqbidv  5812  oveq123d  5874  csbov12g  5892  csbov1g  5893  csbov2g  5894  ovmpodxf  5978  caov42d  6039  caovdilemd  6044  caovimo  6046  offeq  6074  offval2  6076  caofinvl  6083  ot1stg  6131  ot2ndg  6132  2nd1st  6159  mpomptsx  6176  dmmpossx  6178  fmpox  6179  fmpoco  6195  1stconst  6200  algrflemg  6209  tfrexlem  6313  rdgivallem  6360  rdgisuc1  6363  frec0g  6376  frecabcl  6378  frecsuclem  6385  frecrdg  6387  oa0  6436  oasuc  6443  oa1suc  6446  omsuc  6451  nnaass  6464  nndi  6465  nnmass  6466  nnm2  6505  nn2m  6506  ereq1  6520  errn  6535  uniqs2  6573  oviec  6619  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  mapsnconst  6672  mapen  6824  mapxpen  6826  xpmapenlem  6827  phplem4on  6845  fidifsnen  6848  undifdc  6901  fiintim  6906  fisseneq  6909  snexxph  6927  sbthlemi4  6937  sbthlemi6  6939  supeq2  6966  eqsupti  6973  infvalti  6999  djuf1olem  7030  djuss  7047  1stinl  7051  2ndinl  7052  1stinr  7053  2ndinr  7054  updjudhcoinlf  7057  updjudhcoinrg  7058  omp1eomlem  7071  difinfsn  7077  ctmlemr  7085  ctssdclemn0  7087  ctssdc  7090  enumctlemm  7091  nnnninfeq  7104  nnnninfeq2  7105  nninfisollemne  7107  nninfisol  7109  enwomnilem  7145  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  en2other2  7173  cc3  7230  mulidpi  7280  addasspig  7292  mulasspig  7294  distrpig  7295  indpi  7304  addcmpblnq  7329  mulpipq  7334  dmaddpqlem  7339  nqpi  7340  addcomnqg  7343  recrecnq  7356  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltaddnq  7369  ltexnqq  7370  archnqq  7379  prarloclemarch  7380  ltrnqg  7382  ltnnnq  7385  nq0nn  7404  addcmpblnq0  7405  nqpnq0nq  7415  nqnq0a  7416  nq0m0r  7418  nq0a0  7419  distrnq0  7421  addassnq0  7424  nq02m  7427  prarloclemlo  7456  prarloclemcalc  7464  addnqprllem  7489  addnqprulem  7490  addnqprl  7491  addnqpru  7492  appdivnq  7525  mulnqprl  7530  mulnqpru  7531  addcanprlemu  7577  ltaprlem  7580  ltmprr  7604  cauappcvgprlemladdrl  7619  mulcmpblnrlemg  7702  mulcomsrg  7719  distrsrg  7721  ltsosr  7726  1idsr  7730  00sr  7731  ltasrg  7732  recexgt0sr  7735  srpospr  7745  prsradd  7748  prsrriota  7750  caucvgsrlemcau  7755  caucvgsrlemgt1  7757  caucvgsrlemoffval  7758  caucvgsrlemoffres  7762  caucvgsr  7764  map2psrprg  7767  elreal2  7792  mulresr  7800  pitonnlem1p1  7808  pitonnlem2  7809  pitoregt0  7811  recidpirqlemcalc  7819  recidpirq  7820  axaddcl  7826  axmulcl  7828  axmulcom  7833  axmulass  7835  axdistr  7836  ax1rid  7839  axcnre  7843  recriota  7852  axcaucvglemcau  7860  mulid1  7917  mulid2  7918  adddirp1d  7946  joinlmuladdmuld  7947  muladd11  8052  1p1times  8053  readdcan  8059  comraddd  8076  add42  8081  npcan  8128  addsubass  8129  2addsub  8133  addsubeq4  8134  nppcan  8141  nnpcan  8142  npncan2  8146  nncan  8148  subsub  8149  nnncan  8154  nnncan1  8155  pnpcan2  8159  pnncan  8160  subneg  8168  negneg  8169  negdi2  8177  mvrraddd  8285  assraddsubd  8287  subaddeqd  8288  addid0  8292  mul02  8306  mul01  8308  mulneg1  8314  mul2neg  8317  mulm1  8319  ltadd2  8338  rimul  8504  rereim  8505  mulreim  8523  recextlem1  8569  mulcanapd  8579  divcanap1  8598  divrecap2  8606  divmulassap  8612  divmulasscomap  8613  divcanap4  8616  dividap  8618  muldivdirap  8624  divdivdivap  8630  recdivap  8635  divadddivap  8644  divsubdivap  8645  div2negap  8652  divcanap5rd  8735  dmdcanap2d  8738  subrecap  8756  recgt0  8766  lt2mul2div  8795  nnmulcl  8899  times2  9007  add1p1  9127  sub1m1  9128  cnm2m1cnm3  9129  nn0supp  9187  peano2z  9248  nneoor  9314  supminfex  9556  cnref1o  9609  rexneg  9787  xaddpnf1  9803  xaddmnf1  9805  rexadd  9809  xaddid1  9819  xaddid2  9820  xaddass  9826  xpncan  9828  xleadd1a  9830  xltadd1  9833  xposdif  9839  xadd4d  9842  xleaddadd  9844  iooidg  9866  iooval2  9872  icoshftf1o  9948  lincmb01cmp  9960  iccf1o  9961  fzval2  9968  fzsuc  10025  fzpred  10026  fztpval  10039  fseq1p1m1  10050  fzshftral  10064  fz0to4untppr  10080  fzo0to3tp  10175  fzo0sn0fzo1  10177  fzosplitsn  10189  fzosplitprm1  10190  fzisfzounsn  10192  rebtwn2zlemstep  10209  2tnp1ge0ge0  10257  flqdiv  10277  modqvalr  10281  modqdiffl  10291  modqfrac  10293  modqmulnn  10298  modqid  10305  modqcyc  10315  modqcyc2  10316  mulp1mod1  10321  modqmuladd  10322  modqmuladdnn0  10324  qnegmod  10325  m1modnnsub1  10326  addmodid  10328  addmodidr  10329  modqmul12d  10334  modqnegd  10335  modqadd12d  10336  modifeq2int  10342  modqaddmulmod  10347  modqdi  10348  modqsubdir  10349  modsumfzodifsn  10352  addmodlteq  10354  frec2uzsucd  10357  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdglem  10367  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdgdomlem  10373  frecuzrdgfunlem  10375  frecuzrdgtclt  10377  frecuzrdgsuctlem  10379  frecfzennn  10382  seqeq1  10404  seq3val  10414  seqvalcd  10415  seq3p1  10418  seqp1cd  10422  seq3feq2  10426  seq3fveq  10427  seq3shft2  10429  seq3-1p  10436  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemnanb  10446  iseqf1olemqk  10450  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1o  10460  seq3id3  10463  seq3z  10467  fser0const  10472  exp3vallem  10477  expnnval  10479  expp1  10483  expn1ap0  10486  mulexp  10515  expaddzaplem  10519  expaddzap  10520  expmul  10521  expp1zap  10525  expm1ap  10526  sqval  10534  iexpcyc  10580  subsq2  10583  qsqeqor  10586  binom2  10587  binom21  10588  binom2sub1  10590  mulbinom2  10592  binom3  10593  zesq  10594  bernneq  10596  sqoddm1div8  10629  nn0opthlem1d  10654  facp1  10664  faclbnd6  10678  bcval2  10684  bcval3  10685  bcn0  10689  bcp1n  10695  bcp1nk  10696  bcn2  10698  bcp1m1  10699  bcpasc  10700  bcn2m1  10703  hashinfom  10712  hashennn  10714  hashfz1  10717  fseq1hash  10736  omgadd  10737  hashunsng  10742  hashprg  10743  hashdifsn  10754  hashdifpr  10755  hashfz  10756  hashfzo  10757  hashfzo0  10758  hashfzp1  10759  hashfz0  10760  hashxp  10761  resunimafz0  10766  fnfz0hash  10767  ffzo0hash  10769  hashfacen  10771  zfz1isolemsplit  10773  zfz1isolemiso  10774  zfz1isolem1  10775  shftdm  10786  shftval2  10790  shftval4  10792  shftval5  10793  shftcan1  10798  seq3shft  10802  imre  10815  crre  10821  remim  10824  reim0b  10826  recj  10831  reneg  10832  readd  10833  resub  10834  remullem  10835  imcj  10839  imneg  10840  imadd  10841  imsub  10842  cjcj  10847  cjadd  10848  ipcnval  10850  cjneg  10854  cjsub  10856  cjexp  10857  imval2  10858  cjap  10870  resqrexlemf1  10972  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemcalc3  10980  resqrexlemnm  10982  resqrexlemcvg  10983  resqrtcl  10993  sqrtsq  11008  absneg  11014  absvalsq  11017  absvalsq2  11018  sqabsadd  11019  sqabssub  11020  absval2  11021  absreimsq  11031  absmul  11033  absexp  11043  absexpzap  11044  abssuble0  11067  abstri  11068  recan  11073  amgm2  11082  maxabslemlub  11171  max0addsup  11183  minmax  11193  minabs  11199  bdtrilem  11202  bdtri  11203  xrmaxiflemab  11210  xrmaxiflemcom  11212  xrmaxadd  11224  xrminmax  11228  xrmineqinf  11232  xrminrecl  11236  xrbdtri  11239  climshft2  11269  subcn2  11274  reccn2ap  11276  climaddc2  11293  iser3shft  11309  climcvg1nlem  11312  sumeq12dv  11335  sumeq12rdv  11336  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  summodc  11346  fsum3  11350  isumz  11352  fsumf1o  11353  fisumss  11355  fsumsersdc  11358  fsum3ser  11360  fsumsplit  11370  fsumsplitf  11371  sumsnf  11372  fsumsplitsn  11373  fsum1  11375  sumpr  11376  sumtp  11377  fsumm1  11379  fsum1p  11381  fsumsplitsnun  11382  fsump1  11383  isumclim  11384  sumnul  11387  isumadd  11394  fsum2dlemstep  11397  fsumcnv  11400  fisumcom2  11401  fsumshftm  11408  fisumrev2  11409  fisum0diag2  11410  fsumsub  11415  fsumdifsnconst  11418  modfsummodlemstep  11420  fsumabs  11428  telfsumo  11429  telfsum  11431  telfsum2  11432  fsumparts  11433  fsumiun  11440  hashiun  11441  hash2iun  11442  hash2iun1dif1  11443  binomlem  11446  binom1p  11448  binom11  11449  binom1dif  11450  bcxmas  11452  isum1p  11455  isumnn0nn  11456  isumlessdc  11459  divcnv  11460  arisum2  11462  trireciplem  11463  geosergap  11469  geolim  11474  georeclim  11476  geo2lim  11479  geoisum1  11482  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemsumlt  11491  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodfrecap  11509  prodeq12dv  11532  prodeq12rdv  11533  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zprodap0  11544  fprodseq  11546  fprodntrivap  11547  prod1dc  11549  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  prodsnf  11555  fprod1  11557  fprodsplitdc  11559  fprodm1  11561  fprod1p  11562  fprodp1  11563  fprodunsn  11567  fprodcl2lem  11568  fprodabs  11579  fprodconst  11583  fprod2dlemstep  11585  fprodcnv  11588  fprodcom2fi  11589  fprodrec  11592  fprodsplitsn  11596  fprodsplit1f  11597  fprodeq0g  11601  eftabs  11619  efcllemp  11621  ef0lem  11623  efcvgfsum  11630  ege2le3  11634  efcj  11636  efaddlem  11637  efexp  11645  eftlub  11653  efsep  11654  effsumlt  11655  ef4p  11657  efgt1p2  11658  efgt1p  11659  tanval2ap  11676  tanval3ap  11677  resinval  11678  recosval  11679  efi4p  11680  resin4p  11681  recos4p  11682  sinneg  11689  cosneg  11690  tannegap  11691  efmival  11696  sinadd  11699  cosadd  11700  tanaddaplem  11701  tanaddap  11702  sinsub  11703  cossub  11704  addsin  11705  subsin  11706  subcos  11710  sincossq  11711  sin2t  11712  sin01bnd  11720  cos01bnd  11721  absefi  11731  absef  11732  absefib  11733  efieq1re  11734  demoivre  11735  demoivreALT  11736  eirraplem  11739  dvdstr  11790  dvdsadd2b  11802  mulmoddvds  11823  ltoddhalfle  11852  opoe  11854  m1expo  11859  m1exp1  11860  flodddiv4  11893  flodddiv4t2lthalf  11896  zsupcllemstep  11900  nn0gcdid0  11936  gcdaddm  11939  gcdadd  11940  gcdid  11941  gcdabs  11943  modgcd  11946  1gcd  11947  bezout  11966  dfgcd2  11969  mulgcd  11971  absmulgcd  11972  gcdmultiple  11975  gcdmultiplez  11976  rpmulgcd  11981  rplpwr  11982  rppwr  11983  dvdssqlem  11985  uzwodc  11992  ialgr0  11998  alginv  12001  algcvg  12002  algfx  12006  eucalginv  12010  eucalglt  12011  lcmcl  12026  lcmabs  12030  lcmgcdlem  12031  lcmdvds  12033  lcmgcdnn  12036  coprmdvds  12046  qredeq  12050  divgcdcoprm0  12055  divgcdcoprmex  12056  rpexp1i  12108  sqrt2irrlem  12115  sqpweven  12129  2sqpwodd  12130  sqrt2irraplemnn  12133  qmuldeneqnum  12149  nn0gcdsq  12154  numdensq  12156  nn0sqrtelqelz  12160  phibndlem  12170  dfphi2  12174  phiprmpw  12176  phiprm  12177  phimullem  12179  eulerthlem1  12181  eulerthlemh  12185  eulerthlemth  12186  eulerth  12187  prmdiv  12189  hashgcdlem  12192  phisum  12194  odzdvds  12199  vfermltl  12205  powm2modprm  12206  modprm0  12208  nnnn0modprm0  12209  coprimeprodsq  12211  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem4  12222  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem14  12231  pythagtriplem16  12233  pceulem  12248  pcval  12250  pczpre  12251  pcdiv  12256  pc1  12259  pcrec  12262  pcexp  12263  pcid  12277  pcneg  12278  pcgcd1  12281  pc2dvds  12283  difsqpwdvds  12291  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmpt2  12296  pcprod  12298  pcfac  12302  prmpwdvds  12307  pockthlem  12308  1arithlem2  12316  4sqlem9  12338  4sqlem4  12344  mul4sqlem  12345  ennnfonelemp1  12361  ennnfonelemhdmp1  12364  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  ennnfonelemnn0  12377  ctinfomlemom  12382  setsvala  12447  fvsetsid  12450  setsresg  12454  setscom  12456  setsslid  12466  ressid2  12477  ressval2  12478  restid2  12588  lidrididd  12636  grprinvd  12640  mndpropd  12676  mhmf1o  12693  mhmco  12705  grpinvval  12746  isgrpinv  12756  grpsubinv  12772  ntrval  12904  clsval  12905  cldcls  12908  neival  12937  resttop  12964  restco  12968  restabs  12969  resttopon2  12972  cnpval  12992  cnntr  13019  cnrest2  13030  upxp  13066  uptx  13068  cnmpt11  13077  cnmpt21  13085  psmetsym  13123  psmetres2  13127  xmetsym  13162  xmettxlem  13303  txmetcnp  13312  cnbl0  13328  cnblcld  13329  remetdval  13333  bl2ioo  13336  tgioo  13340  addcncntoplem  13345  divcnap  13349  fsumcncntop  13350  cncfmet  13373  cncfmptc  13376  addccncf  13380  negcncf  13382  mulcncflem  13384  ivthinclemlopn  13408  limcimolemlt  13427  cnplimcim  13430  cnplimclemr  13432  limccnp2lem  13439  limccnp2cntop  13440  dvfvalap  13444  dvconst  13455  dvaddxxbr  13459  dvmulxxbr  13460  dvcjbr  13466  dvexp  13469  dvrecap  13471  dvmptclx  13474  dvmptaddx  13475  dvmptmulx  13476  dvmptcmulcn  13477  dveflem  13481  dvef  13482  reeff1oleme  13487  sin0pilem1  13496  sin0pilem2  13497  efper  13522  sinperlem  13523  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  efimpi  13534  ptolemy  13539  sinq12gt0  13545  coseq0negpitopi  13551  tangtx  13553  abssinper  13561  cosq34lt1  13565  relogexp  13587  logdivlti  13596  logcxp  13612  rpcxp0  13613  rpcxp1  13614  1cxp  13615  ecxp  13616  rpcxpadd  13620  rpcxpp1  13621  rpmulcxp  13624  rpdivcxp  13626  cxpmul  13627  rpcxproot  13628  abscxp  13629  rpcxpsqrtth  13644  rplogbid1  13659  rplogb1  13660  rpelogb  13661  rplogbreexp  13665  rplogbzexp  13666  rprelogbmul  13667  rprelogbmulexp  13668  rprelogbdiv  13669  logbrec  13672  rpcxplogb  13676  logbgcd1irr  13679  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  binom4  13691  lgslem1  13695  lgsval2lem  13705  lgsvalmod  13714  lgsneg  13719  lgsdir2lem4  13726  lgsdirprm  13729  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsmodeq  13740  lgsdirnn0  13742  lgsdinn0  13743  2sqlem3  13747  2sqlem4  13748  2sqlem8  13753  djucllem  13835  bj-charfun  13842  bj-charfundc  13843  bj-charfundcALT  13844  nninfsellemeq  14047  nninffeq  14053  qdencn  14059  cvgcmp2nlemabs  14064  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  apdifflemf  14078  redcwlpolemeq1  14086  dceqnconst  14091  dcapnconst  14092  nconstwlpolem0  14094  nconstwlpolemgt0  14095  nconstwlpolem  14096