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  2733  rabeqbidva  2734  csbidmg  3114  csbco3g  3116  difeq12d  3255  ifeq12d  3554  ifbieq1d  3557  ifbieq2d  3559  ifbieq12d  3561  eqifdc  3570  csbsng  3654  disjpr2  3657  csbunig  3818  iuneq12d  3911  unisn3  4446  op1stbg  4480  opthreg  4556  onsucuni2  4564  csbxpg  4708  coeq12d  4792  csbdmg  4822  reseq12d  4909  csbresg  4911  resima2  4942  imaeq12d  4972  csbrng  5091  opswapg  5116  relcnvtr  5149  relcoi2  5160  relcoi1  5161  iotaint  5192  funprg  5267  funtpg  5268  funcnvres2  5292  fnco  5325  fococnv2  5488  fveq12d  5523  csbfv12g  5552  csbfv2g  5553  csbfvg  5554  dffn5im  5562  funfvdm2  5581  fvun1  5583  fvmpt2d  5603  fvmptt  5608  fndmin  5624  fniniseg2  5639  fnniniseg2  5640  fmptcof  5684  fvresi  5710  fvunsng  5711  fvpr1g  5723  fvpr2g  5724  fvtp1g  5725  funiunfvdm  5764  fcof1o  5790  riotaeqbidv  5834  oveq123d  5896  csbov12g  5914  csbov1g  5915  csbov2g  5916  ovmpodxf  6000  caov42d  6061  caovdilemd  6066  caovimo  6068  offeq  6096  offval2  6098  caofinvl  6105  ot1stg  6153  ot2ndg  6154  2nd1st  6181  mpomptsx  6198  dmmpossx  6200  fmpox  6201  fmpoco  6217  1stconst  6222  algrflemg  6231  tfrexlem  6335  rdgivallem  6382  rdgisuc1  6385  frec0g  6398  frecabcl  6400  frecsuclem  6407  frecrdg  6409  oa0  6458  oasuc  6465  oa1suc  6468  omsuc  6473  nnaass  6486  nndi  6487  nnmass  6488  nnm2  6527  nn2m  6528  ereq1  6542  errn  6557  uniqs2  6595  oviec  6641  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  mapsnconst  6694  mapen  6846  mapxpen  6848  xpmapenlem  6849  phplem4on  6867  fidifsnen  6870  undifdc  6923  fiintim  6928  fisseneq  6931  snexxph  6949  sbthlemi4  6959  sbthlemi6  6961  supeq2  6988  eqsupti  6995  infvalti  7021  djuf1olem  7052  djuss  7069  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  updjudhcoinlf  7079  updjudhcoinrg  7080  omp1eomlem  7093  difinfsn  7099  ctmlemr  7107  ctssdclemn0  7109  ctssdc  7112  enumctlemm  7113  nnnninfeq  7126  nnnninfeq2  7127  nninfisollemne  7129  nninfisol  7131  enwomnilem  7167  nninfwlpoimlemg  7173  nninfwlpoimlemginf  7174  en2other2  7195  cc3  7267  mulidpi  7317  addasspig  7329  mulasspig  7331  distrpig  7332  indpi  7341  addcmpblnq  7366  mulpipq  7371  dmaddpqlem  7376  nqpi  7377  addcomnqg  7380  recrecnq  7393  ltsonq  7397  ltanqg  7399  ltmnqg  7400  ltaddnq  7406  ltexnqq  7407  archnqq  7416  prarloclemarch  7417  ltrnqg  7419  ltnnnq  7422  nq0nn  7441  addcmpblnq0  7442  nqpnq0nq  7452  nqnq0a  7453  nq0m0r  7455  nq0a0  7456  distrnq0  7458  addassnq0  7461  nq02m  7464  prarloclemlo  7493  prarloclemcalc  7501  addnqprllem  7526  addnqprulem  7527  addnqprl  7528  addnqpru  7529  appdivnq  7562  mulnqprl  7567  mulnqpru  7568  addcanprlemu  7614  ltaprlem  7617  ltmprr  7641  cauappcvgprlemladdrl  7656  mulcmpblnrlemg  7739  mulcomsrg  7756  distrsrg  7758  ltsosr  7763  1idsr  7767  00sr  7768  ltasrg  7769  recexgt0sr  7772  srpospr  7782  prsradd  7785  prsrriota  7787  caucvgsrlemcau  7792  caucvgsrlemgt1  7794  caucvgsrlemoffval  7795  caucvgsrlemoffres  7799  caucvgsr  7801  map2psrprg  7804  elreal2  7829  mulresr  7837  pitonnlem1p1  7845  pitonnlem2  7846  pitoregt0  7848  recidpirqlemcalc  7856  recidpirq  7857  axaddcl  7863  axmulcl  7865  axmulcom  7870  axmulass  7872  axdistr  7873  ax1rid  7876  axcnre  7880  recriota  7889  axcaucvglemcau  7897  mulrid  7954  mullid  7955  adddirp1d  7984  joinlmuladdmuld  7985  muladd11  8090  1p1times  8091  readdcan  8097  comraddd  8114  add42  8119  npcan  8166  addsubass  8167  2addsub  8171  addsubeq4  8172  nppcan  8179  nnpcan  8180  npncan2  8184  nncan  8186  subsub  8187  nnncan  8192  nnncan1  8193  pnpcan2  8197  pnncan  8198  subneg  8206  negneg  8207  negdi2  8215  mvrraddd  8323  assraddsubd  8325  subaddeqd  8326  addid0  8330  mul02  8344  mul01  8346  mulneg1  8352  mul2neg  8355  mulm1  8357  ltadd2  8376  rimul  8542  rereim  8543  mulreim  8561  recextlem1  8608  mulcanapd  8618  divcanap1  8638  divrecap2  8646  divmulassap  8652  divmulasscomap  8653  divcanap4  8656  dividap  8658  muldivdirap  8664  divdivdivap  8670  recdivap  8675  divadddivap  8684  divsubdivap  8685  div2negap  8692  divcanap5rd  8775  dmdcanap2d  8778  subrecap  8796  recgt0  8807  lt2mul2div  8836  nnmulcl  8940  times2  9048  add1p1  9168  sub1m1  9169  cnm2m1cnm3  9170  nn0supp  9228  peano2z  9289  nneoor  9355  supminfex  9597  cnref1o  9650  rexneg  9830  xaddpnf1  9846  xaddmnf1  9848  rexadd  9852  xaddid1  9862  xaddid2  9863  xaddass  9869  xpncan  9871  xleadd1a  9873  xltadd1  9876  xposdif  9882  xadd4d  9885  xleaddadd  9887  iooidg  9909  iooval2  9915  icoshftf1o  9991  lincmb01cmp  10003  iccf1o  10004  fzval2  10011  fzsuc  10069  fzpred  10070  fztpval  10083  fseq1p1m1  10094  fzshftral  10108  fz0to4untppr  10124  fzo0to3tp  10219  fzo0sn0fzo1  10221  fzosplitsn  10233  fzosplitprm1  10234  fzisfzounsn  10236  rebtwn2zlemstep  10253  2tnp1ge0ge0  10301  flqdiv  10321  modqvalr  10325  modqdiffl  10335  modqfrac  10337  modqmulnn  10342  modqid  10349  modqcyc  10359  modqcyc2  10360  mulp1mod1  10365  modqmuladd  10366  modqmuladdnn0  10368  qnegmod  10369  m1modnnsub1  10370  addmodid  10372  addmodidr  10373  modqmul12d  10378  modqnegd  10379  modqadd12d  10380  modifeq2int  10386  modqaddmulmod  10391  modqdi  10392  modqsubdir  10393  modsumfzodifsn  10396  addmodlteq  10398  frec2uzsucd  10401  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdglem  10411  frecuzrdgsuc  10414  frecuzrdgg  10416  frecuzrdgdomlem  10417  frecuzrdgfunlem  10419  frecuzrdgtclt  10421  frecuzrdgsuctlem  10423  frecfzennn  10426  seqeq1  10448  seq3val  10458  seqvalcd  10459  seq3p1  10462  seqp1cd  10466  seq3feq2  10470  seq3fveq  10471  seq3shft2  10473  seq3-1p  10480  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemnanb  10490  iseqf1olemqk  10494  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3f1o  10504  seq3id3  10507  seq3z  10511  fser0const  10516  exp3vallem  10521  expnnval  10523  expp1  10527  expn1ap0  10530  mulexp  10559  expaddzaplem  10563  expaddzap  10564  expmul  10565  expp1zap  10569  expm1ap  10570  sqval  10578  sqdividap  10585  iexpcyc  10625  subsq2  10628  qsqeqor  10631  binom2  10632  binom21  10633  binom2sub1  10635  mulbinom2  10637  binom3  10638  zesq  10639  bernneq  10641  sqoddm1div8  10674  mulsubdivbinom2ap  10691  nn0opthlem1d  10700  facp1  10710  faclbnd6  10724  bcval2  10730  bcval3  10731  bcn0  10735  bcp1n  10741  bcp1nk  10742  bcn2  10744  bcp1m1  10745  bcpasc  10746  bcn2m1  10749  hashinfom  10758  hashennn  10760  hashfz1  10763  fseq1hash  10781  omgadd  10782  hashunsng  10787  hashprg  10788  hashdifsn  10799  hashdifpr  10800  hashfz  10801  hashfzo  10802  hashfzo0  10803  hashfzp1  10804  hashfz0  10805  hashxp  10806  resunimafz0  10811  fnfz0hash  10812  ffzo0hash  10814  hashfacen  10816  zfz1isolemsplit  10818  zfz1isolemiso  10819  zfz1isolem1  10820  shftdm  10831  shftval2  10835  shftval4  10837  shftval5  10838  shftcan1  10843  seq3shft  10847  imre  10860  crre  10866  remim  10869  reim0b  10871  recj  10876  reneg  10877  readd  10878  resub  10879  remullem  10880  imcj  10884  imneg  10885  imadd  10886  imsub  10887  cjcj  10892  cjadd  10893  ipcnval  10895  cjneg  10899  cjsub  10901  cjexp  10902  imval2  10903  cjap  10915  resqrexlemf1  11017  resqrexlemfp1  11018  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemcvg  11028  resqrtcl  11038  sqrtsq  11053  absneg  11059  absvalsq  11062  absvalsq2  11063  sqabsadd  11064  sqabssub  11065  absval2  11066  absreimsq  11076  absmul  11078  absexp  11088  absexpzap  11089  abssuble0  11112  abstri  11113  recan  11118  amgm2  11127  maxabslemlub  11216  max0addsup  11228  minmax  11238  minabs  11244  bdtrilem  11247  bdtri  11248  xrmaxiflemab  11255  xrmaxiflemcom  11257  xrmaxadd  11269  xrminmax  11273  xrmineqinf  11277  xrminrecl  11281  xrbdtri  11284  climshft2  11314  subcn2  11319  reccn2ap  11321  climaddc2  11338  iser3shft  11354  climcvg1nlem  11357  sumeq12dv  11380  sumeq12rdv  11381  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  summodc  11391  fsum3  11395  isumz  11397  fsumf1o  11398  fisumss  11400  fsumsersdc  11403  fsum3ser  11405  fsumsplit  11415  fsumsplitf  11416  sumsnf  11417  fsumsplitsn  11418  fsum1  11420  sumpr  11421  sumtp  11422  fsumm1  11424  fsum1p  11426  fsumsplitsnun  11427  fsump1  11428  isumclim  11429  sumnul  11432  isumadd  11439  fsum2dlemstep  11442  fsumcnv  11445  fisumcom2  11446  fsumshftm  11453  fisumrev2  11454  fisum0diag2  11455  fsumsub  11460  fsumdifsnconst  11463  modfsummodlemstep  11465  fsumabs  11473  telfsumo  11474  telfsum  11476  telfsum2  11477  fsumparts  11478  fsumiun  11485  hashiun  11486  hash2iun  11487  hash2iun1dif1  11488  binomlem  11491  binom1p  11493  binom11  11494  binom1dif  11495  bcxmas  11497  isum1p  11500  isumnn0nn  11501  isumlessdc  11504  divcnv  11505  arisum2  11507  trireciplem  11508  geosergap  11514  geolim  11519  georeclim  11521  geo2lim  11524  geoisum1  11527  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemsumlt  11536  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodfrecap  11554  prodeq12dv  11577  prodeq12rdv  11578  prodrbdclem  11579  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  zprodap0  11589  fprodseq  11591  fprodntrivap  11592  prod1dc  11594  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  prodsnf  11600  fprod1  11602  fprodsplitdc  11604  fprodm1  11606  fprod1p  11607  fprodp1  11608  fprodunsn  11612  fprodcl2lem  11613  fprodabs  11624  fprodconst  11628  fprod2dlemstep  11630  fprodcnv  11633  fprodcom2fi  11634  fprodrec  11637  fprodsplitsn  11641  fprodsplit1f  11642  fprodeq0g  11646  eftabs  11664  efcllemp  11666  ef0lem  11668  efcvgfsum  11675  ege2le3  11679  efcj  11681  efaddlem  11682  efexp  11690  eftlub  11698  efsep  11699  effsumlt  11700  ef4p  11702  efgt1p2  11703  efgt1p  11704  tanval2ap  11721  tanval3ap  11722  resinval  11723  recosval  11724  efi4p  11725  resin4p  11726  recos4p  11727  sinneg  11734  cosneg  11735  tannegap  11736  efmival  11741  sinadd  11744  cosadd  11745  tanaddaplem  11746  tanaddap  11747  sinsub  11748  cossub  11749  addsin  11750  subsin  11751  subcos  11755  sincossq  11756  sin2t  11757  sin01bnd  11765  cos01bnd  11766  absefi  11776  absef  11777  absefib  11778  efieq1re  11779  demoivre  11780  demoivreALT  11781  eirraplem  11784  dvdstr  11835  dvdsadd2b  11847  mulmoddvds  11869  ltoddhalfle  11898  opoe  11900  m1expo  11905  m1exp1  11906  flodddiv4  11939  flodddiv4t2lthalf  11942  zsupcllemstep  11946  nn0gcdid0  11982  gcdaddm  11985  gcdadd  11986  gcdid  11987  gcdabs  11989  modgcd  11992  1gcd  11993  bezout  12012  dfgcd2  12015  mulgcd  12017  absmulgcd  12018  gcdmultiple  12021  gcdmultiplez  12022  rpmulgcd  12027  rplpwr  12028  rppwr  12029  dvdssqlem  12031  uzwodc  12038  ialgr0  12044  alginv  12047  algcvg  12048  algfx  12052  eucalginv  12056  eucalglt  12057  lcmcl  12072  lcmabs  12076  lcmgcdlem  12077  lcmdvds  12079  lcmgcdnn  12082  coprmdvds  12092  qredeq  12096  divgcdcoprm0  12101  divgcdcoprmex  12102  rpexp1i  12154  sqrt2irrlem  12161  sqpweven  12175  2sqpwodd  12176  sqrt2irraplemnn  12179  qmuldeneqnum  12195  nn0gcdsq  12200  numdensq  12202  nn0sqrtelqelz  12206  phibndlem  12216  dfphi2  12220  phiprmpw  12222  phiprm  12223  phimullem  12225  eulerthlem1  12227  eulerthlemh  12231  eulerthlemth  12232  eulerth  12233  prmdiv  12235  hashgcdlem  12238  phisum  12240  odzdvds  12245  vfermltl  12251  powm2modprm  12252  modprm0  12254  nnnn0modprm0  12255  coprimeprodsq  12257  pythagtriplem1  12265  pythagtriplem3  12267  pythagtriplem4  12268  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem14  12277  pythagtriplem16  12279  pceulem  12294  pcval  12296  pczpre  12297  pcdiv  12302  pc1  12305  pcrec  12308  pcexp  12309  pcid  12323  pcneg  12324  pcgcd1  12327  pc2dvds  12329  difsqpwdvds  12337  pcaddlem  12338  pcadd  12339  pcmpt  12341  pcmpt2  12342  pcprod  12344  pcfac  12348  prmpwdvds  12353  pockthlem  12354  1arithlem2  12362  4sqlem9  12384  4sqlem4  12390  mul4sqlem  12391  ennnfonelemp1  12407  ennnfonelemhdmp1  12410  ennnfonelemss  12411  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  ennnfonelemnn0  12423  ctinfomlemom  12428  setsvala  12493  fvsetsid  12496  setsresg  12500  setscom  12502  setsslid  12513  ressbasd  12527  ressabsg  12535  restid2  12697  prdsex  12718  imasex  12726  imasival  12727  qusval  12744  xpsff1o  12768  lidrididd  12801  grprinvd  12805  mndpropd  12841  mhmf1o  12861  mhmco  12874  grpinvval  12916  isgrpinv  12926  grpsubinv  12943  grpidssd  12946  grpinvsub  12952  grpsubid  12954  grpsubadd0sub  12957  grpsubsub  12959  grpnpncan0  12966  grpnnncan2  12967  grpsubpropd2  12975  grp1inv  12977  ghmgrp  12982  mulgnn  12989  mulgnnp1  12991  mulg2  12992  mulgnegnn  12993  mulgneg  13001  mulgnegneg  13002  mulgm1  13003  mulgaddcom  13007  mulginvcom  13008  mulgnn0z  13010  mulgz  13011  mulgnn0dir  13013  mulgdirlem  13014  mulgp1  13016  mulgnnass  13018  mulgnn0ass  13019  mulgass  13020  mulgassr  13021  mhmmulg  13024  mulgpropdg  13025  subg0  13040  subgmulg  13048  issubg4m  13053  isnsg3  13067  nmzsubg  13070  0nsg  13074  eqger  13083  eqgid  13085  eqgcpbl  13087  rinvmod  13112  ablsub4  13116  ablpncan3  13120  ablnnncan  13126  ablnnncan1  13127  mgptopng  13139  srgass  13154  srgmulgass  13172  srgpcomp  13173  srgpcomppsc  13175  srglmhm  13176  srgrmhm  13177  ringcom  13214  ringpropd  13217  crngpropd  13218  isringd  13220  iscrngd  13221  ringinvnzdiv  13227  ringnegl  13228  ringnegr  13229  ringsubdi  13233  ringsubdir  13234  mulgass2  13235  opprmulg  13243  opprring  13249  oppr1g  13252  isunitd  13275  unitmulcl  13282  unitgrp  13285  invrfvald  13291  dvrid  13306  dvrcan1  13309  rdivmuldivd  13313  rngidpropdg  13315  unitpropdg  13317  invrpropdg  13318  subrguss  13357  subrgdv  13359  subrgunit  13360  subrgpropd  13369  aprval  13372  islmod  13381  islmodd  13383  lmodvs0  13412  lmodvsmmulgdi  13413  lmodfopne  13416  lmodcom  13423  lmodnegadd  13426  lmodsubvs  13433  lmodsubdir  13435  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  cncrng  13466  zsssubrg  13482  ntrval  13613  clsval  13614  cldcls  13617  neival  13646  resttop  13673  restco  13677  restabs  13678  resttopon2  13681  cnpval  13701  cnntr  13728  cnrest2  13739  upxp  13775  uptx  13777  cnmpt11  13786  cnmpt21  13794  psmetsym  13832  psmetres2  13836  xmetsym  13871  xmettxlem  14012  txmetcnp  14021  cnbl0  14037  cnblcld  14038  remetdval  14042  bl2ioo  14045  tgioo  14049  addcncntoplem  14054  divcnap  14058  fsumcncntop  14059  cncfmet  14082  cncfmptc  14085  addccncf  14089  negcncf  14091  mulcncflem  14093  ivthinclemlopn  14117  limcimolemlt  14136  cnplimcim  14139  cnplimclemr  14141  limccnp2lem  14148  limccnp2cntop  14149  dvfvalap  14153  dvconst  14164  dvaddxxbr  14168  dvmulxxbr  14169  dvcjbr  14175  dvexp  14178  dvrecap  14180  dvmptclx  14183  dvmptaddx  14184  dvmptmulx  14185  dvmptcmulcn  14186  dveflem  14190  dvef  14191  reeff1oleme  14196  sin0pilem1  14205  sin0pilem2  14206  efper  14231  sinperlem  14232  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  efimpi  14243  ptolemy  14248  sinq12gt0  14254  coseq0negpitopi  14260  tangtx  14262  abssinper  14270  cosq34lt1  14274  relogexp  14296  logdivlti  14305  logcxp  14321  rpcxp0  14322  rpcxp1  14323  1cxp  14324  ecxp  14325  rpcxpadd  14329  rpcxpp1  14330  rpmulcxp  14333  rpdivcxp  14335  cxpmul  14336  rpcxproot  14337  abscxp  14338  rpcxpsqrtth  14353  rplogbid1  14368  rplogb1  14369  rpelogb  14370  rplogbreexp  14374  rplogbzexp  14375  rprelogbmul  14376  rprelogbmulexp  14377  rprelogbdiv  14378  logbrec  14381  rpcxplogb  14385  logbgcd1irr  14388  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  binom4  14400  lgslem1  14404  lgsval2lem  14414  lgsvalmod  14423  lgsneg  14428  lgsdir2lem4  14435  lgsdirprm  14438  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsmodeq  14449  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem1  14456  2lgsoddprmlem2  14457  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  djucllem  14555  bj-charfun  14562  bj-charfundc  14563  bj-charfundcALT  14564  nninfsellemeq  14766  nninffeq  14772  qdencn  14778  cvgcmp2nlemabs  14783  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  apdifflemf  14797  redcwlpolemeq1  14805  dceqnconst  14810  dcapnconst  14811  nconstwlpolem0  14813  nconstwlpolemgt0  14814  nconstwlpolem  14815