Theorem eqtrd 2198

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

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtr2d  2199  eqtr3d  2200  eqtr4d  2201  3eqtrd  2202  3eqtrrd  2203  3eqtr2d  2204  syl5eq  2210  eqtrdi  2214  rabeqbidv  2720  rabeqbidva  2721  csbidmg  3100  csbco3g  3102  difeq12d  3240  ifeq12d  3538  ifbieq1d  3541  ifbieq2d  3543  ifbieq12d  3545  eqifdc  3553  csbsng  3636  disjpr2  3639  csbunig  3796  iuneq12d  3889  unisn3  4422  op1stbg  4456  opthreg  4532  onsucuni2  4540  csbxpg  4684  coeq12d  4767  csbdmg  4797  reseq12d  4884  csbresg  4886  resima2  4917  imaeq12d  4946  csbrng  5064  opswapg  5089  relcnvtr  5122  relcoi2  5133  relcoi1  5134  iotaint  5165  funprg  5237  funtpg  5238  funcnvres2  5262  fnco  5295  fococnv2  5457  fveq12d  5492  csbfv12g  5521  csbfv2g  5522  csbfvg  5523  dffn5im  5531  funfvdm2  5549  fvun1  5551  fvmpt2d  5571  fvmptt  5576  fndmin  5591  fniniseg2  5606  fnniniseg2  5607  fmptcof  5651  fvresi  5677  fvunsng  5678  fvpr1g  5690  fvpr2g  5691  fvtp1g  5692  funiunfvdm  5730  fcof1o  5756  riotaeqbidv  5800  oveq123d  5862  csbov12g  5877  csbov1g  5878  csbov2g  5879  ovmpodxf  5963  caov42d  6024  caovdilemd  6029  caovimo  6031  grprinvd  6033  offeq  6062  offval2  6064  caofinvl  6071  ot1stg  6117  ot2ndg  6118  2nd1st  6145  mpomptsx  6162  dmmpossx  6164  fmpox  6165  fmpoco  6180  1stconst  6185  algrflemg  6194  tfrexlem  6298  rdgivallem  6345  rdgisuc1  6348  frec0g  6361  frecabcl  6363  frecsuclem  6370  frecrdg  6372  oa0  6421  oasuc  6428  oa1suc  6431  omsuc  6436  nnaass  6449  nndi  6450  nnmass  6451  nnm2  6489  nn2m  6490  ereq1  6504  errn  6519  uniqs2  6557  oviec  6603  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  mapsnconst  6656  mapen  6808  mapxpen  6810  xpmapenlem  6811  phplem4on  6829  fidifsnen  6832  undifdc  6885  fiintim  6890  fisseneq  6893  snexxph  6911  sbthlemi4  6921  sbthlemi6  6923  supeq2  6950  eqsupti  6957  infvalti  6983  djuf1olem  7014  djuss  7031  1stinl  7035  2ndinl  7036  1stinr  7037  2ndinr  7038  updjudhcoinlf  7041  updjudhcoinrg  7042  omp1eomlem  7055  difinfsn  7061  ctmlemr  7069  ctssdclemn0  7071  ctssdc  7074  enumctlemm  7075  nnnninfeq  7088  nnnninfeq2  7089  nninfisollemne  7091  nninfisol  7093  enwomnilem  7129  en2other2  7148  cc3  7205  mulidpi  7255  addasspig  7267  mulasspig  7269  distrpig  7270  indpi  7279  addcmpblnq  7304  mulpipq  7309  dmaddpqlem  7314  nqpi  7315  addcomnqg  7318  recrecnq  7331  ltsonq  7335  ltanqg  7337  ltmnqg  7338  ltaddnq  7344  ltexnqq  7345  archnqq  7354  prarloclemarch  7355  ltrnqg  7357  ltnnnq  7360  nq0nn  7379  addcmpblnq0  7380  nqpnq0nq  7390  nqnq0a  7391  nq0m0r  7393  nq0a0  7394  distrnq0  7396  addassnq0  7399  nq02m  7402  prarloclemlo  7431  prarloclemcalc  7439  addnqprllem  7464  addnqprulem  7465  addnqprl  7466  addnqpru  7467  appdivnq  7500  mulnqprl  7505  mulnqpru  7506  addcanprlemu  7552  ltaprlem  7555  ltmprr  7579  cauappcvgprlemladdrl  7594  mulcmpblnrlemg  7677  mulcomsrg  7694  distrsrg  7696  ltsosr  7701  1idsr  7705  00sr  7706  ltasrg  7707  recexgt0sr  7710  srpospr  7720  prsradd  7723  prsrriota  7725  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffval  7733  caucvgsrlemoffres  7737  caucvgsr  7739  map2psrprg  7742  elreal2  7767  mulresr  7775  pitonnlem1p1  7783  pitonnlem2  7784  pitoregt0  7786  recidpirqlemcalc  7794  recidpirq  7795  axaddcl  7801  axmulcl  7803  axmulcom  7808  axmulass  7810  axdistr  7811  ax1rid  7814  axcnre  7818  recriota  7827  axcaucvglemcau  7835  mulid1  7892  mulid2  7893  adddirp1d  7921  joinlmuladdmuld  7922  muladd11  8027  1p1times  8028  readdcan  8034  comraddd  8051  add42  8056  npcan  8103  addsubass  8104  2addsub  8108  addsubeq4  8109  nppcan  8116  nnpcan  8117  npncan2  8121  nncan  8123  subsub  8124  nnncan  8129  nnncan1  8130  pnpcan2  8134  pnncan  8135  subneg  8143  negneg  8144  negdi2  8152  mvrraddd  8260  assraddsubd  8262  subaddeqd  8263  addid0  8267  mul02  8281  mul01  8283  mulneg1  8289  mul2neg  8292  mulm1  8294  ltadd2  8313  rimul  8479  rereim  8480  mulreim  8498  recextlem1  8544  mulcanapd  8554  divcanap1  8573  divrecap2  8581  divmulassap  8587  divmulasscomap  8588  divcanap4  8591  dividap  8593  muldivdirap  8599  divdivdivap  8605  recdivap  8610  divadddivap  8619  divsubdivap  8620  div2negap  8627  divcanap5rd  8710  dmdcanap2d  8713  subrecap  8731  recgt0  8741  lt2mul2div  8770  nnmulcl  8874  times2  8982  add1p1  9102  sub1m1  9103  cnm2m1cnm3  9104  nn0supp  9162  peano2z  9223  nneoor  9289  supminfex  9531  cnref1o  9584  rexneg  9762  xaddpnf1  9778  xaddmnf1  9780  rexadd  9784  xaddid1  9794  xaddid2  9795  xaddass  9801  xpncan  9803  xleadd1a  9805  xltadd1  9808  xposdif  9814  xadd4d  9817  xleaddadd  9819  iooidg  9841  iooval2  9847  icoshftf1o  9923  lincmb01cmp  9935  iccf1o  9936  fzval2  9943  fzsuc  10000  fzpred  10001  fztpval  10014  fseq1p1m1  10025  fzshftral  10039  fz0to4untppr  10055  fzo0to3tp  10150  fzo0sn0fzo1  10152  fzosplitsn  10164  fzosplitprm1  10165  fzisfzounsn  10167  rebtwn2zlemstep  10184  2tnp1ge0ge0  10232  flqdiv  10252  modqvalr  10256  modqdiffl  10266  modqfrac  10268  modqmulnn  10273  modqid  10280  modqcyc  10290  modqcyc2  10291  mulp1mod1  10296  modqmuladd  10297  modqmuladdnn0  10299  qnegmod  10300  m1modnnsub1  10301  addmodid  10303  addmodidr  10304  modqmul12d  10309  modqnegd  10310  modqadd12d  10311  modifeq2int  10317  modqaddmulmod  10322  modqdi  10323  modqsubdir  10324  modsumfzodifsn  10327  addmodlteq  10329  frec2uzsucd  10332  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdglem  10342  frecuzrdgsuc  10345  frecuzrdgg  10347  frecuzrdgdomlem  10348  frecuzrdgfunlem  10350  frecuzrdgtclt  10352  frecuzrdgsuctlem  10354  frecfzennn  10357  seqeq1  10379  seq3val  10389  seqvalcd  10390  seq3p1  10393  seqp1cd  10397  seq3feq2  10401  seq3fveq  10402  seq3shft2  10404  seq3-1p  10411  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemnanb  10421  iseqf1olemqk  10425  iseqf1olemfvp  10428  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1o  10435  seq3id3  10438  seq3z  10442  fser0const  10447  exp3vallem  10452  expnnval  10454  expp1  10458  expn1ap0  10461  mulexp  10490  expaddzaplem  10494  expaddzap  10495  expmul  10496  expp1zap  10500  expm1ap  10501  sqval  10509  iexpcyc  10555  subsq2  10558  qsqeqor  10561  binom2  10562  binom21  10563  binom2sub1  10565  mulbinom2  10567  binom3  10568  zesq  10569  bernneq  10571  sqoddm1div8  10604  nn0opthlem1d  10629  facp1  10639  faclbnd6  10653  bcval2  10659  bcval3  10660  bcn0  10664  bcp1n  10670  bcp1nk  10671  bcn2  10673  bcp1m1  10674  bcpasc  10675  bcn2m1  10678  hashinfom  10687  hashennn  10689  hashfz1  10692  fseq1hash  10710  omgadd  10711  hashunsng  10716  hashprg  10717  hashdifsn  10728  hashdifpr  10729  hashfz  10730  hashfzo  10731  hashfzo0  10732  hashfzp1  10733  hashfz0  10734  hashxp  10735  resunimafz0  10740  fnfz0hash  10741  ffzo0hash  10743  hashfacen  10745  zfz1isolemsplit  10747  zfz1isolemiso  10748  zfz1isolem1  10749  shftdm  10760  shftval2  10764  shftval4  10766  shftval5  10767  shftcan1  10772  seq3shft  10776  imre  10789  crre  10795  remim  10798  reim0b  10800  recj  10805  reneg  10806  readd  10807  resub  10808  remullem  10809  imcj  10813  imneg  10814  imadd  10815  imsub  10816  cjcj  10821  cjadd  10822  ipcnval  10824  cjneg  10828  cjsub  10830  cjexp  10831  imval2  10832  cjap  10844  resqrexlemf1  10946  resqrexlemfp1  10947  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemcvg  10957  resqrtcl  10967  sqrtsq  10982  absneg  10988  absvalsq  10991  absvalsq2  10992  sqabsadd  10993  sqabssub  10994  absval2  10995  absreimsq  11005  absmul  11007  absexp  11017  absexpzap  11018  abssuble0  11041  abstri  11042  recan  11047  amgm2  11056  maxabslemlub  11145  max0addsup  11157  minmax  11167  minabs  11173  bdtrilem  11176  bdtri  11177  xrmaxiflemab  11184  xrmaxiflemcom  11186  xrmaxadd  11198  xrminmax  11202  xrmineqinf  11206  xrminrecl  11210  xrbdtri  11213  climshft2  11243  subcn2  11248  reccn2ap  11250  climaddc2  11267  iser3shft  11283  climcvg1nlem  11286  sumeq12dv  11309  sumeq12rdv  11310  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  summodc  11320  fsum3  11324  isumz  11326  fsumf1o  11327  fisumss  11329  fsumsersdc  11332  fsum3ser  11334  fsumsplit  11344  fsumsplitf  11345  sumsnf  11346  fsumsplitsn  11347  fsum1  11349  sumpr  11350  sumtp  11351  fsumm1  11353  fsum1p  11355  fsumsplitsnun  11356  fsump1  11357  isumclim  11358  sumnul  11361  isumadd  11368  fsum2dlemstep  11371  fsumcnv  11374  fisumcom2  11375  fsumshftm  11382  fisumrev2  11383  fisum0diag2  11384  fsumsub  11389  fsumdifsnconst  11392  modfsummodlemstep  11394  fsumabs  11402  telfsumo  11403  telfsum  11405  telfsum2  11406  fsumparts  11407  fsumiun  11414  hashiun  11415  hash2iun  11416  hash2iun1dif1  11417  binomlem  11420  binom1p  11422  binom11  11423  binom1dif  11424  bcxmas  11426  isum1p  11429  isumnn0nn  11430  isumlessdc  11433  divcnv  11434  arisum2  11436  trireciplem  11437  geosergap  11443  geolim  11448  georeclim  11450  geo2lim  11453  geoisum1  11456  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemsumlt  11465  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodfrecap  11483  prodeq12dv  11506  prodeq12rdv  11507  prodrbdclem  11508  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  zprodap0  11518  fprodseq  11520  fprodntrivap  11521  prod1dc  11523  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  prodsnf  11529  fprod1  11531  fprodsplitdc  11533  fprodm1  11535  fprod1p  11536  fprodp1  11537  fprodunsn  11541  fprodcl2lem  11542  fprodabs  11553  fprodconst  11557  fprod2dlemstep  11559  fprodcnv  11562  fprodcom2fi  11563  fprodrec  11566  fprodsplitsn  11570  fprodsplit1f  11571  fprodeq0g  11575  eftabs  11593  efcllemp  11595  ef0lem  11597  efcvgfsum  11604  ege2le3  11608  efcj  11610  efaddlem  11611  efexp  11619  eftlub  11627  efsep  11628  effsumlt  11629  ef4p  11631  efgt1p2  11632  efgt1p  11633  tanval2ap  11650  tanval3ap  11651  resinval  11652  recosval  11653  efi4p  11654  resin4p  11655  recos4p  11656  sinneg  11663  cosneg  11664  tannegap  11665  efmival  11670  sinadd  11673  cosadd  11674  tanaddaplem  11675  tanaddap  11676  sinsub  11677  cossub  11678  addsin  11679  subsin  11680  subcos  11684  sincossq  11685  sin2t  11686  sin01bnd  11694  cos01bnd  11695  absefi  11705  absef  11706  absefib  11707  efieq1re  11708  demoivre  11709  demoivreALT  11710  eirraplem  11713  dvdstr  11764  dvdsadd2b  11776  mulmoddvds  11797  ltoddhalfle  11826  opoe  11828  m1expo  11833  m1exp1  11834  flodddiv4  11867  flodddiv4t2lthalf  11870  zsupcllemstep  11874  nn0gcdid0  11910  gcdaddm  11913  gcdadd  11914  gcdid  11915  gcdabs  11917  modgcd  11920  1gcd  11921  bezout  11940  dfgcd2  11943  mulgcd  11945  absmulgcd  11946  gcdmultiple  11949  gcdmultiplez  11950  rpmulgcd  11955  rplpwr  11956  rppwr  11957  dvdssqlem  11959  uzwodc  11966  ialgr0  11972  alginv  11975  algcvg  11976  algfx  11980  eucalginv  11984  eucalglt  11985  lcmcl  12000  lcmabs  12004  lcmgcdlem  12005  lcmdvds  12007  lcmgcdnn  12010  coprmdvds  12020  qredeq  12024  divgcdcoprm0  12029  divgcdcoprmex  12030  rpexp1i  12082  sqrt2irrlem  12089  sqpweven  12103  2sqpwodd  12104  sqrt2irraplemnn  12107  qmuldeneqnum  12123  nn0gcdsq  12128  numdensq  12130  nn0sqrtelqelz  12134  phibndlem  12144  dfphi2  12148  phiprmpw  12150  phiprm  12151  phimullem  12153  eulerthlem1  12155  eulerthlemh  12159  eulerthlemth  12160  eulerth  12161  prmdiv  12163  hashgcdlem  12166  phisum  12168  odzdvds  12173  vfermltl  12179  powm2modprm  12180  modprm0  12182  nnnn0modprm0  12183  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem14  12205  pythagtriplem16  12207  pceulem  12222  pcval  12224  pczpre  12225  pcdiv  12230  pc1  12233  pcrec  12236  pcexp  12237  pcid  12251  pcneg  12252  pcgcd1  12255  pc2dvds  12257  difsqpwdvds  12265  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcmpt2  12270  pcprod  12272  pcfac  12276  prmpwdvds  12281  pockthlem  12282  1arithlem2  12290  4sqlem9  12312  4sqlem4  12318  mul4sqlem  12319  ennnfonelemp1  12335  ennnfonelemhdmp1  12338  ennnfonelemss  12339  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemhom  12344  ennnfonelemnn0  12351  ctinfomlemom  12356  setsvala  12421  fvsetsid  12424  setsresg  12428  setscom  12430  setsslid  12440  ressid2  12449  ressval2  12450  restid2  12560  ntrval  12710  clsval  12711  cldcls  12714  neival  12743  resttop  12770  restco  12774  restabs  12775  resttopon2  12778  cnpval  12798  cnntr  12825  cnrest2  12836  upxp  12872  uptx  12874  cnmpt11  12883  cnmpt21  12891  psmetsym  12929  psmetres2  12933  xmetsym  12968  xmettxlem  13109  txmetcnp  13118  cnbl0  13134  cnblcld  13135  remetdval  13139  bl2ioo  13142  tgioo  13146  addcncntoplem  13151  divcnap  13155  fsumcncntop  13156  cncfmet  13179  cncfmptc  13182  addccncf  13186  negcncf  13188  mulcncflem  13190  ivthinclemlopn  13214  limcimolemlt  13233  cnplimcim  13236  cnplimclemr  13238  limccnp2lem  13245  limccnp2cntop  13246  dvfvalap  13250  dvconst  13261  dvaddxxbr  13265  dvmulxxbr  13266  dvcjbr  13272  dvexp  13275  dvrecap  13277  dvmptclx  13280  dvmptaddx  13281  dvmptmulx  13282  dvmptcmulcn  13283  dveflem  13287  dvef  13288  reeff1oleme  13293  sin0pilem1  13302  sin0pilem2  13303  efper  13328  sinperlem  13329  sinmpi  13336  cosmpi  13337  sinppi  13338  cosppi  13339  efimpi  13340  ptolemy  13345  sinq12gt0  13351  coseq0negpitopi  13357  tangtx  13359  abssinper  13367  cosq34lt1  13371  relogexp  13393  logdivlti  13402  logcxp  13418  rpcxp0  13419  rpcxp1  13420  1cxp  13421  ecxp  13422  rpcxpadd  13426  rpcxpp1  13427  rpmulcxp  13430  rpdivcxp  13432  cxpmul  13433  rpcxproot  13434  abscxp  13435  rpcxpsqrtth  13450  rplogbid1  13465  rplogb1  13466  rpelogb  13467  rplogbreexp  13471  rplogbzexp  13472  rprelogbmul  13473  rprelogbmulexp  13474  rprelogbdiv  13475  logbrec  13478  rpcxplogb  13482  logbgcd1irr  13485  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  binom4  13497  lgslem1  13501  lgsval2lem  13511  lgsvalmod  13520  lgsneg  13525  lgsdir2lem4  13532  lgsdirprm  13535  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsmodeq  13546  lgsdirnn0  13548  lgsdinn0  13549  2sqlem3  13553  2sqlem4  13554  2sqlem8  13559  djucllem  13641  bj-charfun  13649  bj-charfundc  13650  bj-charfundcALT  13651  nninfsellemeq  13854  nninffeq  13860  qdencn  13866  cvgcmp2nlemabs  13871  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  apdifflemf  13885  redcwlpolemeq1  13893  dceqnconst  13898  dcapnconst  13899  nconstwlpolem0  13901  nconstwlpolemgt0  13902  nconstwlpolem  13903