Theorem eqtrd 2208

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 2187	. 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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  eqtr2d  2209  eqtr3d  2210  eqtr4d  2211  3eqtrd  2212  3eqtrrd  2213  3eqtr2d  2214  eqtrid  2220  eqtrdi  2224  rabeqbidv  2730  rabeqbidva  2731  csbidmg  3111  csbco3g  3113  difeq12d  3252  ifeq12d  3551  ifbieq1d  3554  ifbieq2d  3556  ifbieq12d  3558  eqifdc  3566  csbsng  3650  disjpr2  3653  csbunig  3813  iuneq12d  3906  unisn3  4439  op1stbg  4473  opthreg  4549  onsucuni2  4557  csbxpg  4701  coeq12d  4784  csbdmg  4814  reseq12d  4901  csbresg  4903  resima2  4934  imaeq12d  4964  csbrng  5082  opswapg  5107  relcnvtr  5140  relcoi2  5151  relcoi1  5152  iotaint  5183  funprg  5258  funtpg  5259  funcnvres2  5283  fnco  5316  fococnv2  5479  fveq12d  5514  csbfv12g  5543  csbfv2g  5544  csbfvg  5545  dffn5im  5553  funfvdm2  5572  fvun1  5574  fvmpt2d  5594  fvmptt  5599  fndmin  5615  fniniseg2  5630  fnniniseg2  5631  fmptcof  5675  fvresi  5701  fvunsng  5702  fvpr1g  5714  fvpr2g  5715  fvtp1g  5716  funiunfvdm  5754  fcof1o  5780  riotaeqbidv  5824  oveq123d  5886  csbov12g  5904  csbov1g  5905  csbov2g  5906  ovmpodxf  5990  caov42d  6051  caovdilemd  6056  caovimo  6058  offeq  6086  offval2  6088  caofinvl  6095  ot1stg  6143  ot2ndg  6144  2nd1st  6171  mpomptsx  6188  dmmpossx  6190  fmpox  6191  fmpoco  6207  1stconst  6212  algrflemg  6221  tfrexlem  6325  rdgivallem  6372  rdgisuc1  6375  frec0g  6388  frecabcl  6390  frecsuclem  6397  frecrdg  6399  oa0  6448  oasuc  6455  oa1suc  6458  omsuc  6463  nnaass  6476  nndi  6477  nnmass  6478  nnm2  6517  nn2m  6518  ereq1  6532  errn  6547  uniqs2  6585  oviec  6631  ecovass  6634  ecoviass  6635  ecovdi  6636  ecovidi  6637  mapsnconst  6684  mapen  6836  mapxpen  6838  xpmapenlem  6839  phplem4on  6857  fidifsnen  6860  undifdc  6913  fiintim  6918  fisseneq  6921  snexxph  6939  sbthlemi4  6949  sbthlemi6  6951  supeq2  6978  eqsupti  6985  infvalti  7011  djuf1olem  7042  djuss  7059  1stinl  7063  2ndinl  7064  1stinr  7065  2ndinr  7066  updjudhcoinlf  7069  updjudhcoinrg  7070  omp1eomlem  7083  difinfsn  7089  ctmlemr  7097  ctssdclemn0  7099  ctssdc  7102  enumctlemm  7103  nnnninfeq  7116  nnnninfeq2  7117  nninfisollemne  7119  nninfisol  7121  enwomnilem  7157  nninfwlpoimlemg  7163  nninfwlpoimlemginf  7164  en2other2  7185  cc3  7242  mulidpi  7292  addasspig  7304  mulasspig  7306  distrpig  7307  indpi  7316  addcmpblnq  7341  mulpipq  7346  dmaddpqlem  7351  nqpi  7352  addcomnqg  7355  recrecnq  7368  ltsonq  7372  ltanqg  7374  ltmnqg  7375  ltaddnq  7381  ltexnqq  7382  archnqq  7391  prarloclemarch  7392  ltrnqg  7394  ltnnnq  7397  nq0nn  7416  addcmpblnq0  7417  nqpnq0nq  7427  nqnq0a  7428  nq0m0r  7430  nq0a0  7431  distrnq0  7433  addassnq0  7436  nq02m  7439  prarloclemlo  7468  prarloclemcalc  7476  addnqprllem  7501  addnqprulem  7502  addnqprl  7503  addnqpru  7504  appdivnq  7537  mulnqprl  7542  mulnqpru  7543  addcanprlemu  7589  ltaprlem  7592  ltmprr  7616  cauappcvgprlemladdrl  7631  mulcmpblnrlemg  7714  mulcomsrg  7731  distrsrg  7733  ltsosr  7738  1idsr  7742  00sr  7743  ltasrg  7744  recexgt0sr  7747  srpospr  7757  prsradd  7760  prsrriota  7762  caucvgsrlemcau  7767  caucvgsrlemgt1  7769  caucvgsrlemoffval  7770  caucvgsrlemoffres  7774  caucvgsr  7776  map2psrprg  7779  elreal2  7804  mulresr  7812  pitonnlem1p1  7820  pitonnlem2  7821  pitoregt0  7823  recidpirqlemcalc  7831  recidpirq  7832  axaddcl  7838  axmulcl  7840  axmulcom  7845  axmulass  7847  axdistr  7848  ax1rid  7851  axcnre  7855  recriota  7864  axcaucvglemcau  7872  mulid1  7929  mulid2  7930  adddirp1d  7958  joinlmuladdmuld  7959  muladd11  8064  1p1times  8065  readdcan  8071  comraddd  8088  add42  8093  npcan  8140  addsubass  8141  2addsub  8145  addsubeq4  8146  nppcan  8153  nnpcan  8154  npncan2  8158  nncan  8160  subsub  8161  nnncan  8166  nnncan1  8167  pnpcan2  8171  pnncan  8172  subneg  8180  negneg  8181  negdi2  8189  mvrraddd  8297  assraddsubd  8299  subaddeqd  8300  addid0  8304  mul02  8318  mul01  8320  mulneg1  8326  mul2neg  8329  mulm1  8331  ltadd2  8350  rimul  8516  rereim  8517  mulreim  8535  recextlem1  8581  mulcanapd  8591  divcanap1  8610  divrecap2  8618  divmulassap  8624  divmulasscomap  8625  divcanap4  8628  dividap  8630  muldivdirap  8636  divdivdivap  8642  recdivap  8647  divadddivap  8656  divsubdivap  8657  div2negap  8664  divcanap5rd  8747  dmdcanap2d  8750  subrecap  8768  recgt0  8778  lt2mul2div  8807  nnmulcl  8911  times2  9019  add1p1  9139  sub1m1  9140  cnm2m1cnm3  9141  nn0supp  9199  peano2z  9260  nneoor  9326  supminfex  9568  cnref1o  9621  rexneg  9799  xaddpnf1  9815  xaddmnf1  9817  rexadd  9821  xaddid1  9831  xaddid2  9832  xaddass  9838  xpncan  9840  xleadd1a  9842  xltadd1  9845  xposdif  9851  xadd4d  9854  xleaddadd  9856  iooidg  9878  iooval2  9884  icoshftf1o  9960  lincmb01cmp  9972  iccf1o  9973  fzval2  9980  fzsuc  10037  fzpred  10038  fztpval  10051  fseq1p1m1  10062  fzshftral  10076  fz0to4untppr  10092  fzo0to3tp  10187  fzo0sn0fzo1  10189  fzosplitsn  10201  fzosplitprm1  10202  fzisfzounsn  10204  rebtwn2zlemstep  10221  2tnp1ge0ge0  10269  flqdiv  10289  modqvalr  10293  modqdiffl  10303  modqfrac  10305  modqmulnn  10310  modqid  10317  modqcyc  10327  modqcyc2  10328  mulp1mod1  10333  modqmuladd  10334  modqmuladdnn0  10336  qnegmod  10337  m1modnnsub1  10338  addmodid  10340  addmodidr  10341  modqmul12d  10346  modqnegd  10347  modqadd12d  10348  modifeq2int  10354  modqaddmulmod  10359  modqdi  10360  modqsubdir  10361  modsumfzodifsn  10364  addmodlteq  10366  frec2uzsucd  10369  frecuzrdgrrn  10376  frec2uzrdg  10377  frecuzrdglem  10379  frecuzrdgsuc  10382  frecuzrdgg  10384  frecuzrdgdomlem  10385  frecuzrdgfunlem  10387  frecuzrdgtclt  10389  frecuzrdgsuctlem  10391  frecfzennn  10394  seqeq1  10416  seq3val  10426  seqvalcd  10427  seq3p1  10430  seqp1cd  10434  seq3feq2  10438  seq3fveq  10439  seq3shft2  10441  seq3-1p  10448  iseqf1olemnab  10456  iseqf1olemab  10457  iseqf1olemnanb  10458  iseqf1olemqk  10462  iseqf1olemfvp  10465  seq3f1olemqsumkj  10466  seq3f1olemqsumk  10467  seq3f1olemqsum  10468  seq3f1o  10472  seq3id3  10475  seq3z  10479  fser0const  10484  exp3vallem  10489  expnnval  10491  expp1  10495  expn1ap0  10498  mulexp  10527  expaddzaplem  10531  expaddzap  10532  expmul  10533  expp1zap  10537  expm1ap  10538  sqval  10546  iexpcyc  10592  subsq2  10595  qsqeqor  10598  binom2  10599  binom21  10600  binom2sub1  10602  mulbinom2  10604  binom3  10605  zesq  10606  bernneq  10608  sqoddm1div8  10641  nn0opthlem1d  10666  facp1  10676  faclbnd6  10690  bcval2  10696  bcval3  10697  bcn0  10701  bcp1n  10707  bcp1nk  10708  bcn2  10710  bcp1m1  10711  bcpasc  10712  bcn2m1  10715  hashinfom  10724  hashennn  10726  hashfz1  10729  fseq1hash  10747  omgadd  10748  hashunsng  10753  hashprg  10754  hashdifsn  10765  hashdifpr  10766  hashfz  10767  hashfzo  10768  hashfzo0  10769  hashfzp1  10770  hashfz0  10771  hashxp  10772  resunimafz0  10777  fnfz0hash  10778  ffzo0hash  10780  hashfacen  10782  zfz1isolemsplit  10784  zfz1isolemiso  10785  zfz1isolem1  10786  shftdm  10797  shftval2  10801  shftval4  10803  shftval5  10804  shftcan1  10809  seq3shft  10813  imre  10826  crre  10832  remim  10835  reim0b  10837  recj  10842  reneg  10843  readd  10844  resub  10845  remullem  10846  imcj  10850  imneg  10851  imadd  10852  imsub  10853  cjcj  10858  cjadd  10859  ipcnval  10861  cjneg  10865  cjsub  10867  cjexp  10868  imval2  10869  cjap  10881  resqrexlemf1  10983  resqrexlemfp1  10984  resqrexlemover  10985  resqrexlemcalc1  10989  resqrexlemcalc3  10991  resqrexlemnm  10993  resqrexlemcvg  10994  resqrtcl  11004  sqrtsq  11019  absneg  11025  absvalsq  11028  absvalsq2  11029  sqabsadd  11030  sqabssub  11031  absval2  11032  absreimsq  11042  absmul  11044  absexp  11054  absexpzap  11055  abssuble0  11078  abstri  11079  recan  11084  amgm2  11093  maxabslemlub  11182  max0addsup  11194  minmax  11204  minabs  11210  bdtrilem  11213  bdtri  11214  xrmaxiflemab  11221  xrmaxiflemcom  11223  xrmaxadd  11235  xrminmax  11239  xrmineqinf  11243  xrminrecl  11247  xrbdtri  11250  climshft2  11280  subcn2  11285  reccn2ap  11287  climaddc2  11304  iser3shft  11320  climcvg1nlem  11323  sumeq12dv  11346  sumeq12rdv  11347  sumrbdclem  11351  fsum3cvg  11352  summodclem3  11354  summodclem2a  11355  summodc  11357  fsum3  11361  isumz  11363  fsumf1o  11364  fisumss  11366  fsumsersdc  11369  fsum3ser  11371  fsumsplit  11381  fsumsplitf  11382  sumsnf  11383  fsumsplitsn  11384  fsum1  11386  sumpr  11387  sumtp  11388  fsumm1  11390  fsum1p  11392  fsumsplitsnun  11393  fsump1  11394  isumclim  11395  sumnul  11398  isumadd  11405  fsum2dlemstep  11408  fsumcnv  11411  fisumcom2  11412  fsumshftm  11419  fisumrev2  11420  fisum0diag2  11421  fsumsub  11426  fsumdifsnconst  11429  modfsummodlemstep  11431  fsumabs  11439  telfsumo  11440  telfsum  11442  telfsum2  11443  fsumparts  11444  fsumiun  11451  hashiun  11452  hash2iun  11453  hash2iun1dif1  11454  binomlem  11457  binom1p  11459  binom11  11460  binom1dif  11461  bcxmas  11463  isum1p  11466  isumnn0nn  11467  isumlessdc  11470  divcnv  11471  arisum2  11473  trireciplem  11474  geosergap  11480  geolim  11485  georeclim  11487  geo2lim  11490  geoisum1  11493  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  cvgratnnlemsumlt  11502  cvgratz  11506  mertenslemi1  11509  mertenslem2  11510  mertensabs  11511  prodfrecap  11520  prodeq12dv  11543  prodeq12rdv  11544  prodrbdclem  11545  fproddccvg  11546  prodmodclem3  11549  prodmodclem2a  11550  zprodap0  11555  fprodseq  11557  fprodntrivap  11558  prod1dc  11560  fprodf1o  11562  prodssdc  11563  fprodssdc  11564  prodsnf  11566  fprod1  11568  fprodsplitdc  11570  fprodm1  11572  fprod1p  11573  fprodp1  11574  fprodunsn  11578  fprodcl2lem  11579  fprodabs  11590  fprodconst  11594  fprod2dlemstep  11596  fprodcnv  11599  fprodcom2fi  11600  fprodrec  11603  fprodsplitsn  11607  fprodsplit1f  11608  fprodeq0g  11612  eftabs  11630  efcllemp  11632  ef0lem  11634  efcvgfsum  11641  ege2le3  11645  efcj  11647  efaddlem  11648  efexp  11656  eftlub  11664  efsep  11665  effsumlt  11666  ef4p  11668  efgt1p2  11669  efgt1p  11670  tanval2ap  11687  tanval3ap  11688  resinval  11689  recosval  11690  efi4p  11691  resin4p  11692  recos4p  11693  sinneg  11700  cosneg  11701  tannegap  11702  efmival  11707  sinadd  11710  cosadd  11711  tanaddaplem  11712  tanaddap  11713  sinsub  11714  cossub  11715  addsin  11716  subsin  11717  subcos  11721  sincossq  11722  sin2t  11723  sin01bnd  11731  cos01bnd  11732  absefi  11742  absef  11743  absefib  11744  efieq1re  11745  demoivre  11746  demoivreALT  11747  eirraplem  11750  dvdstr  11801  dvdsadd2b  11813  mulmoddvds  11834  ltoddhalfle  11863  opoe  11865  m1expo  11870  m1exp1  11871  flodddiv4  11904  flodddiv4t2lthalf  11907  zsupcllemstep  11911  nn0gcdid0  11947  gcdaddm  11950  gcdadd  11951  gcdid  11952  gcdabs  11954  modgcd  11957  1gcd  11958  bezout  11977  dfgcd2  11980  mulgcd  11982  absmulgcd  11983  gcdmultiple  11986  gcdmultiplez  11987  rpmulgcd  11992  rplpwr  11993  rppwr  11994  dvdssqlem  11996  uzwodc  12003  ialgr0  12009  alginv  12012  algcvg  12013  algfx  12017  eucalginv  12021  eucalglt  12022  lcmcl  12037  lcmabs  12041  lcmgcdlem  12042  lcmdvds  12044  lcmgcdnn  12047  coprmdvds  12057  qredeq  12061  divgcdcoprm0  12066  divgcdcoprmex  12067  rpexp1i  12119  sqrt2irrlem  12126  sqpweven  12140  2sqpwodd  12141  sqrt2irraplemnn  12144  qmuldeneqnum  12160  nn0gcdsq  12165  numdensq  12167  nn0sqrtelqelz  12171  phibndlem  12181  dfphi2  12185  phiprmpw  12187  phiprm  12188  phimullem  12190  eulerthlem1  12192  eulerthlemh  12196  eulerthlemth  12197  eulerth  12198  prmdiv  12200  hashgcdlem  12203  phisum  12205  odzdvds  12210  vfermltl  12216  powm2modprm  12217  modprm0  12219  nnnn0modprm0  12220  coprimeprodsq  12222  pythagtriplem1  12230  pythagtriplem3  12232  pythagtriplem4  12233  pythagtriplem6  12235  pythagtriplem7  12236  pythagtriplem14  12242  pythagtriplem16  12244  pceulem  12259  pcval  12261  pczpre  12262  pcdiv  12267  pc1  12270  pcrec  12273  pcexp  12274  pcid  12288  pcneg  12289  pcgcd1  12292  pc2dvds  12294  difsqpwdvds  12302  pcaddlem  12303  pcadd  12304  pcmpt  12306  pcmpt2  12307  pcprod  12309  pcfac  12313  prmpwdvds  12318  pockthlem  12319  1arithlem2  12327  4sqlem9  12349  4sqlem4  12355  mul4sqlem  12356  ennnfonelemp1  12372  ennnfonelemhdmp1  12375  ennnfonelemss  12376  ennnfonelemkh  12378  ennnfonelemhf1o  12379  ennnfonelemhom  12381  ennnfonelemnn0  12388  ctinfomlemom  12393  setsvala  12458  fvsetsid  12461  setsresg  12465  setscom  12467  setsslid  12477  ressid2  12488  ressval2  12489  restid2  12617  lidrididd  12665  grprinvd  12669  mndpropd  12705  mhmf1o  12722  mhmco  12734  grpinvval  12776  isgrpinv  12786  grpsubinv  12802  grpidssd  12805  grpinvsub  12811  grpsubid  12813  grpsubadd0sub  12816  grpsubsub  12818  grpnpncan0  12825  grpnnncan2  12826  grpsubpropd2  12834  grp1inv  12836  ghmgrp  12841  mulgnn  12848  mulgnnp1  12850  mulg2  12851  mulgnegnn  12852  mulgneg  12860  mulgnegneg  12861  mulgm1  12862  mulgaddcom  12865  mulginvcom  12866  mulgnn0z  12868  mulgz  12869  mulgnn0dir  12871  mulgdirlem  12872  mulgp1  12874  mulgnnass  12876  mulgnn0ass  12877  mulgass  12878  mulgassr  12879  mhmmulg  12882  mulgpropdg  12883  rinvmod  12909  ablsub4  12913  ablpncan3  12917  ablnnncan  12923  ablnnncan1  12924  mgptopng  12935  srgass  12949  srgmulgass  12967  srgpcomp  12968  srgpcomppsc  12970  srglmhm  12971  srgrmhm  12972  ringcom  13008  ringpropd  13011  crngpropd  13012  isringd  13014  iscrngd  13015  ringinvnzdiv  13021  ringnegl  13022  rngnegr  13023  ringsubdi  13027  rngsubdir  13028  mulgass2  13029  opprmulg  13036  opprring  13042  oppr1g  13045  ntrval  13179  clsval  13180  cldcls  13183  neival  13212  resttop  13239  restco  13243  restabs  13244  resttopon2  13247  cnpval  13267  cnntr  13294  cnrest2  13305  upxp  13341  uptx  13343  cnmpt11  13352  cnmpt21  13360  psmetsym  13398  psmetres2  13402  xmetsym  13437  xmettxlem  13578  txmetcnp  13587  cnbl0  13603  cnblcld  13604  remetdval  13608  bl2ioo  13611  tgioo  13615  addcncntoplem  13620  divcnap  13624  fsumcncntop  13625  cncfmet  13648  cncfmptc  13651  addccncf  13655  negcncf  13657  mulcncflem  13659  ivthinclemlopn  13683  limcimolemlt  13702  cnplimcim  13705  cnplimclemr  13707  limccnp2lem  13714  limccnp2cntop  13715  dvfvalap  13719  dvconst  13730  dvaddxxbr  13734  dvmulxxbr  13735  dvcjbr  13741  dvexp  13744  dvrecap  13746  dvmptclx  13749  dvmptaddx  13750  dvmptmulx  13751  dvmptcmulcn  13752  dveflem  13756  dvef  13757  reeff1oleme  13762  sin0pilem1  13771  sin0pilem2  13772  efper  13797  sinperlem  13798  sinmpi  13805  cosmpi  13806  sinppi  13807  cosppi  13808  efimpi  13809  ptolemy  13814  sinq12gt0  13820  coseq0negpitopi  13826  tangtx  13828  abssinper  13836  cosq34lt1  13840  relogexp  13862  logdivlti  13871  logcxp  13887  rpcxp0  13888  rpcxp1  13889  1cxp  13890  ecxp  13891  rpcxpadd  13895  rpcxpp1  13896  rpmulcxp  13899  rpdivcxp  13901  cxpmul  13902  rpcxproot  13903  abscxp  13904  rpcxpsqrtth  13919  rplogbid1  13934  rplogb1  13935  rpelogb  13936  rplogbreexp  13940  rplogbzexp  13941  rprelogbmul  13942  rprelogbmulexp  13943  rprelogbdiv  13944  logbrec  13947  rpcxplogb  13951  logbgcd1irr  13954  logbgcd1irraplemexp  13955  logbgcd1irraplemap  13956  binom4  13966  lgslem1  13970  lgsval2lem  13980  lgsvalmod  13989  lgsneg  13994  lgsdir2lem4  14001  lgsdirprm  14004  lgsdir  14005  lgsdilem2  14006  lgsdi  14007  lgsne0  14008  lgsmodeq  14015  lgsdirnn0  14017  lgsdinn0  14018  2sqlem3  14022  2sqlem4  14023  2sqlem8  14028  djucllem  14110  bj-charfun  14117  bj-charfundc  14118  bj-charfundcALT  14119  nninfsellemeq  14322  nninffeq  14328  qdencn  14334  cvgcmp2nlemabs  14339  trilpolemisumle  14345  trilpolemeq1  14347  trilpolemlt1  14348  apdifflemf  14353  redcwlpolemeq1  14361  dceqnconst  14366  dcapnconst  14367  nconstwlpolem0  14369  nconstwlpolemgt0  14370  nconstwlpolem  14371