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  2732  rabeqbidva  2733  csbidmg  3113  csbco3g  3115  difeq12d  3254  ifeq12d  3553  ifbieq1d  3556  ifbieq2d  3558  ifbieq12d  3560  eqifdc  3569  csbsng  3653  disjpr2  3656  csbunig  3817  iuneq12d  3910  unisn3  4445  op1stbg  4479  opthreg  4555  onsucuni2  4563  csbxpg  4707  coeq12d  4791  csbdmg  4821  reseq12d  4908  csbresg  4910  resima2  4941  imaeq12d  4971  csbrng  5090  opswapg  5115  relcnvtr  5148  relcoi2  5159  relcoi1  5160  iotaint  5191  funprg  5266  funtpg  5267  funcnvres2  5291  fnco  5324  fococnv2  5487  fveq12d  5522  csbfv12g  5551  csbfv2g  5552  csbfvg  5553  dffn5im  5561  funfvdm2  5580  fvun1  5582  fvmpt2d  5602  fvmptt  5607  fndmin  5623  fniniseg2  5638  fnniniseg2  5639  fmptcof  5683  fvresi  5709  fvunsng  5710  fvpr1g  5722  fvpr2g  5723  fvtp1g  5724  funiunfvdm  5763  fcof1o  5789  riotaeqbidv  5833  oveq123d  5895  csbov12g  5913  csbov1g  5914  csbov2g  5915  ovmpodxf  5999  caov42d  6060  caovdilemd  6065  caovimo  6067  offeq  6095  offval2  6097  caofinvl  6104  ot1stg  6152  ot2ndg  6153  2nd1st  6180  mpomptsx  6197  dmmpossx  6199  fmpox  6200  fmpoco  6216  1stconst  6221  algrflemg  6230  tfrexlem  6334  rdgivallem  6381  rdgisuc1  6384  frec0g  6397  frecabcl  6399  frecsuclem  6406  frecrdg  6408  oa0  6457  oasuc  6464  oa1suc  6467  omsuc  6472  nnaass  6485  nndi  6486  nnmass  6487  nnm2  6526  nn2m  6527  ereq1  6541  errn  6556  uniqs2  6594  oviec  6640  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  mapsnconst  6693  mapen  6845  mapxpen  6847  xpmapenlem  6848  phplem4on  6866  fidifsnen  6869  undifdc  6922  fiintim  6927  fisseneq  6930  snexxph  6948  sbthlemi4  6958  sbthlemi6  6960  supeq2  6987  eqsupti  6994  infvalti  7020  djuf1olem  7051  djuss  7068  1stinl  7072  2ndinl  7073  1stinr  7074  2ndinr  7075  updjudhcoinlf  7078  updjudhcoinrg  7079  omp1eomlem  7092  difinfsn  7098  ctmlemr  7106  ctssdclemn0  7108  ctssdc  7111  enumctlemm  7112  nnnninfeq  7125  nnnninfeq2  7126  nninfisollemne  7128  nninfisol  7130  enwomnilem  7166  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  en2other2  7194  cc3  7266  mulidpi  7316  addasspig  7328  mulasspig  7330  distrpig  7331  indpi  7340  addcmpblnq  7365  mulpipq  7370  dmaddpqlem  7375  nqpi  7376  addcomnqg  7379  recrecnq  7392  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltaddnq  7405  ltexnqq  7406  archnqq  7415  prarloclemarch  7416  ltrnqg  7418  ltnnnq  7421  nq0nn  7440  addcmpblnq0  7441  nqpnq0nq  7451  nqnq0a  7452  nq0m0r  7454  nq0a0  7455  distrnq0  7457  addassnq0  7460  nq02m  7463  prarloclemlo  7492  prarloclemcalc  7500  addnqprllem  7525  addnqprulem  7526  addnqprl  7527  addnqpru  7528  appdivnq  7561  mulnqprl  7566  mulnqpru  7567  addcanprlemu  7613  ltaprlem  7616  ltmprr  7640  cauappcvgprlemladdrl  7655  mulcmpblnrlemg  7738  mulcomsrg  7755  distrsrg  7757  ltsosr  7762  1idsr  7766  00sr  7767  ltasrg  7768  recexgt0sr  7771  srpospr  7781  prsradd  7784  prsrriota  7786  caucvgsrlemcau  7791  caucvgsrlemgt1  7793  caucvgsrlemoffval  7794  caucvgsrlemoffres  7798  caucvgsr  7800  map2psrprg  7803  elreal2  7828  mulresr  7836  pitonnlem1p1  7844  pitonnlem2  7845  pitoregt0  7847  recidpirqlemcalc  7855  recidpirq  7856  axaddcl  7862  axmulcl  7864  axmulcom  7869  axmulass  7871  axdistr  7872  ax1rid  7875  axcnre  7879  recriota  7888  axcaucvglemcau  7896  mulrid  7953  mullid  7954  adddirp1d  7983  joinlmuladdmuld  7984  muladd11  8089  1p1times  8090  readdcan  8096  comraddd  8113  add42  8118  npcan  8165  addsubass  8166  2addsub  8170  addsubeq4  8171  nppcan  8178  nnpcan  8179  npncan2  8183  nncan  8185  subsub  8186  nnncan  8191  nnncan1  8192  pnpcan2  8196  pnncan  8197  subneg  8205  negneg  8206  negdi2  8214  mvrraddd  8322  assraddsubd  8324  subaddeqd  8325  addid0  8329  mul02  8343  mul01  8345  mulneg1  8351  mul2neg  8354  mulm1  8356  ltadd2  8375  rimul  8541  rereim  8542  mulreim  8560  recextlem1  8607  mulcanapd  8617  divcanap1  8637  divrecap2  8645  divmulassap  8651  divmulasscomap  8652  divcanap4  8655  dividap  8657  muldivdirap  8663  divdivdivap  8669  recdivap  8674  divadddivap  8683  divsubdivap  8684  div2negap  8691  divcanap5rd  8774  dmdcanap2d  8777  subrecap  8795  recgt0  8806  lt2mul2div  8835  nnmulcl  8939  times2  9047  add1p1  9167  sub1m1  9168  cnm2m1cnm3  9169  nn0supp  9227  peano2z  9288  nneoor  9354  supminfex  9596  cnref1o  9649  rexneg  9829  xaddpnf1  9845  xaddmnf1  9847  rexadd  9851  xaddid1  9861  xaddid2  9862  xaddass  9868  xpncan  9870  xleadd1a  9872  xltadd1  9875  xposdif  9881  xadd4d  9884  xleaddadd  9886  iooidg  9908  iooval2  9914  icoshftf1o  9990  lincmb01cmp  10002  iccf1o  10003  fzval2  10010  fzsuc  10068  fzpred  10069  fztpval  10082  fseq1p1m1  10093  fzshftral  10107  fz0to4untppr  10123  fzo0to3tp  10218  fzo0sn0fzo1  10220  fzosplitsn  10232  fzosplitprm1  10233  fzisfzounsn  10235  rebtwn2zlemstep  10252  2tnp1ge0ge0  10300  flqdiv  10320  modqvalr  10324  modqdiffl  10334  modqfrac  10336  modqmulnn  10341  modqid  10348  modqcyc  10358  modqcyc2  10359  mulp1mod1  10364  modqmuladd  10365  modqmuladdnn0  10367  qnegmod  10368  m1modnnsub1  10369  addmodid  10371  addmodidr  10372  modqmul12d  10377  modqnegd  10378  modqadd12d  10379  modifeq2int  10385  modqaddmulmod  10390  modqdi  10391  modqsubdir  10392  modsumfzodifsn  10395  addmodlteq  10397  frec2uzsucd  10400  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdglem  10410  frecuzrdgsuc  10413  frecuzrdgg  10415  frecuzrdgdomlem  10416  frecuzrdgfunlem  10418  frecuzrdgtclt  10420  frecuzrdgsuctlem  10422  frecfzennn  10425  seqeq1  10447  seq3val  10457  seqvalcd  10458  seq3p1  10461  seqp1cd  10465  seq3feq2  10469  seq3fveq  10470  seq3shft2  10472  seq3-1p  10479  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemnanb  10489  iseqf1olemqk  10493  iseqf1olemfvp  10496  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1o  10503  seq3id3  10506  seq3z  10510  fser0const  10515  exp3vallem  10520  expnnval  10522  expp1  10526  expn1ap0  10529  mulexp  10558  expaddzaplem  10562  expaddzap  10563  expmul  10564  expp1zap  10568  expm1ap  10569  sqval  10577  sqdividap  10584  iexpcyc  10624  subsq2  10627  qsqeqor  10630  binom2  10631  binom21  10632  binom2sub1  10634  mulbinom2  10636  binom3  10637  zesq  10638  bernneq  10640  sqoddm1div8  10673  mulsubdivbinom2ap  10690  nn0opthlem1d  10699  facp1  10709  faclbnd6  10723  bcval2  10729  bcval3  10730  bcn0  10734  bcp1n  10740  bcp1nk  10741  bcn2  10743  bcp1m1  10744  bcpasc  10745  bcn2m1  10748  hashinfom  10757  hashennn  10759  hashfz1  10762  fseq1hash  10780  omgadd  10781  hashunsng  10786  hashprg  10787  hashdifsn  10798  hashdifpr  10799  hashfz  10800  hashfzo  10801  hashfzo0  10802  hashfzp1  10803  hashfz0  10804  hashxp  10805  resunimafz0  10810  fnfz0hash  10811  ffzo0hash  10813  hashfacen  10815  zfz1isolemsplit  10817  zfz1isolemiso  10818  zfz1isolem1  10819  shftdm  10830  shftval2  10834  shftval4  10836  shftval5  10837  shftcan1  10842  seq3shft  10846  imre  10859  crre  10865  remim  10868  reim0b  10870  recj  10875  reneg  10876  readd  10877  resub  10878  remullem  10879  imcj  10883  imneg  10884  imadd  10885  imsub  10886  cjcj  10891  cjadd  10892  ipcnval  10894  cjneg  10898  cjsub  10900  cjexp  10901  imval2  10902  cjap  10914  resqrexlemf1  11016  resqrexlemfp1  11017  resqrexlemover  11018  resqrexlemcalc1  11022  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemcvg  11027  resqrtcl  11037  sqrtsq  11052  absneg  11058  absvalsq  11061  absvalsq2  11062  sqabsadd  11063  sqabssub  11064  absval2  11065  absreimsq  11075  absmul  11077  absexp  11087  absexpzap  11088  abssuble0  11111  abstri  11112  recan  11117  amgm2  11126  maxabslemlub  11215  max0addsup  11227  minmax  11237  minabs  11243  bdtrilem  11246  bdtri  11247  xrmaxiflemab  11254  xrmaxiflemcom  11256  xrmaxadd  11268  xrminmax  11272  xrmineqinf  11276  xrminrecl  11280  xrbdtri  11283  climshft2  11313  subcn2  11318  reccn2ap  11320  climaddc2  11337  iser3shft  11353  climcvg1nlem  11356  sumeq12dv  11379  sumeq12rdv  11380  sumrbdclem  11384  fsum3cvg  11385  summodclem3  11387  summodclem2a  11388  summodc  11390  fsum3  11394  isumz  11396  fsumf1o  11397  fisumss  11399  fsumsersdc  11402  fsum3ser  11404  fsumsplit  11414  fsumsplitf  11415  sumsnf  11416  fsumsplitsn  11417  fsum1  11419  sumpr  11420  sumtp  11421  fsumm1  11423  fsum1p  11425  fsumsplitsnun  11426  fsump1  11427  isumclim  11428  sumnul  11431  isumadd  11438  fsum2dlemstep  11441  fsumcnv  11444  fisumcom2  11445  fsumshftm  11452  fisumrev2  11453  fisum0diag2  11454  fsumsub  11459  fsumdifsnconst  11462  modfsummodlemstep  11464  fsumabs  11472  telfsumo  11473  telfsum  11475  telfsum2  11476  fsumparts  11477  fsumiun  11484  hashiun  11485  hash2iun  11486  hash2iun1dif1  11487  binomlem  11490  binom1p  11492  binom11  11493  binom1dif  11494  bcxmas  11496  isum1p  11499  isumnn0nn  11500  isumlessdc  11503  divcnv  11504  arisum2  11506  trireciplem  11507  geosergap  11513  geolim  11518  georeclim  11520  geo2lim  11523  geoisum1  11526  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemsumlt  11535  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodfrecap  11553  prodeq12dv  11576  prodeq12rdv  11577  prodrbdclem  11578  fproddccvg  11579  prodmodclem3  11582  prodmodclem2a  11583  zprodap0  11588  fprodseq  11590  fprodntrivap  11591  prod1dc  11593  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  prodsnf  11599  fprod1  11601  fprodsplitdc  11603  fprodm1  11605  fprod1p  11606  fprodp1  11607  fprodunsn  11611  fprodcl2lem  11612  fprodabs  11623  fprodconst  11627  fprod2dlemstep  11629  fprodcnv  11632  fprodcom2fi  11633  fprodrec  11636  fprodsplitsn  11640  fprodsplit1f  11641  fprodeq0g  11645  eftabs  11663  efcllemp  11665  ef0lem  11667  efcvgfsum  11674  ege2le3  11678  efcj  11680  efaddlem  11681  efexp  11689  eftlub  11697  efsep  11698  effsumlt  11699  ef4p  11701  efgt1p2  11702  efgt1p  11703  tanval2ap  11720  tanval3ap  11721  resinval  11722  recosval  11723  efi4p  11724  resin4p  11725  recos4p  11726  sinneg  11733  cosneg  11734  tannegap  11735  efmival  11740  sinadd  11743  cosadd  11744  tanaddaplem  11745  tanaddap  11746  sinsub  11747  cossub  11748  addsin  11749  subsin  11750  subcos  11754  sincossq  11755  sin2t  11756  sin01bnd  11764  cos01bnd  11765  absefi  11775  absef  11776  absefib  11777  efieq1re  11778  demoivre  11779  demoivreALT  11780  eirraplem  11783  dvdstr  11834  dvdsadd2b  11846  mulmoddvds  11868  ltoddhalfle  11897  opoe  11899  m1expo  11904  m1exp1  11905  flodddiv4  11938  flodddiv4t2lthalf  11941  zsupcllemstep  11945  nn0gcdid0  11981  gcdaddm  11984  gcdadd  11985  gcdid  11986  gcdabs  11988  modgcd  11991  1gcd  11992  bezout  12011  dfgcd2  12014  mulgcd  12016  absmulgcd  12017  gcdmultiple  12020  gcdmultiplez  12021  rpmulgcd  12026  rplpwr  12027  rppwr  12028  dvdssqlem  12030  uzwodc  12037  ialgr0  12043  alginv  12046  algcvg  12047  algfx  12051  eucalginv  12055  eucalglt  12056  lcmcl  12071  lcmabs  12075  lcmgcdlem  12076  lcmdvds  12078  lcmgcdnn  12081  coprmdvds  12091  qredeq  12095  divgcdcoprm0  12100  divgcdcoprmex  12101  rpexp1i  12153  sqrt2irrlem  12160  sqpweven  12174  2sqpwodd  12175  sqrt2irraplemnn  12178  qmuldeneqnum  12194  nn0gcdsq  12199  numdensq  12201  nn0sqrtelqelz  12205  phibndlem  12215  dfphi2  12219  phiprmpw  12221  phiprm  12222  phimullem  12224  eulerthlem1  12226  eulerthlemh  12230  eulerthlemth  12231  eulerth  12232  prmdiv  12234  hashgcdlem  12237  phisum  12239  odzdvds  12244  vfermltl  12250  powm2modprm  12251  modprm0  12253  nnnn0modprm0  12254  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem3  12266  pythagtriplem4  12267  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem14  12276  pythagtriplem16  12278  pceulem  12293  pcval  12295  pczpre  12296  pcdiv  12301  pc1  12304  pcrec  12307  pcexp  12308  pcid  12322  pcneg  12323  pcgcd1  12326  pc2dvds  12328  difsqpwdvds  12336  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmpt2  12341  pcprod  12343  pcfac  12347  prmpwdvds  12352  pockthlem  12353  1arithlem2  12361  4sqlem9  12383  4sqlem4  12389  mul4sqlem  12390  ennnfonelemp1  12406  ennnfonelemhdmp1  12409  ennnfonelemss  12410  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemhom  12415  ennnfonelemnn0  12422  ctinfomlemom  12427  setsvala  12492  fvsetsid  12495  setsresg  12499  setscom  12501  setsslid  12512  ressbasd  12526  ressabsg  12534  restid2  12696  prdsex  12717  imasex  12725  imasival  12726  qusval  12743  xpsff1o  12767  lidrididd  12800  grprinvd  12804  mndpropd  12840  mhmf1o  12860  mhmco  12873  grpinvval  12915  isgrpinv  12925  grpsubinv  12942  grpidssd  12945  grpinvsub  12951  grpsubid  12953  grpsubadd0sub  12956  grpsubsub  12958  grpnpncan0  12965  grpnnncan2  12966  grpsubpropd2  12974  grp1inv  12976  ghmgrp  12981  mulgnn  12988  mulgnnp1  12990  mulg2  12991  mulgnegnn  12992  mulgneg  13000  mulgnegneg  13001  mulgm1  13002  mulgaddcom  13005  mulginvcom  13006  mulgnn0z  13008  mulgz  13009  mulgnn0dir  13011  mulgdirlem  13012  mulgp1  13014  mulgnnass  13016  mulgnn0ass  13017  mulgass  13018  mulgassr  13019  mhmmulg  13022  mulgpropdg  13023  subg0  13038  subgmulg  13046  issubg4m  13051  isnsg3  13065  nmzsubg  13068  0nsg  13072  eqger  13081  eqgid  13083  eqgcpbl  13085  rinvmod  13110  ablsub4  13114  ablpncan3  13118  ablnnncan  13124  ablnnncan1  13125  mgptopng  13137  srgass  13152  srgmulgass  13170  srgpcomp  13171  srgpcomppsc  13173  srglmhm  13174  srgrmhm  13175  ringcom  13212  ringpropd  13215  crngpropd  13216  isringd  13218  iscrngd  13219  ringinvnzdiv  13225  ringnegl  13226  rngnegr  13227  ringsubdi  13231  rngsubdir  13232  mulgass2  13233  opprmulg  13241  opprring  13247  oppr1g  13250  isunitd  13273  unitmulcl  13280  unitgrp  13283  invrfvald  13289  dvrid  13304  dvrcan1  13307  rdivmuldivd  13311  rngidpropdg  13313  unitpropdg  13315  invrpropdg  13316  subrguss  13355  subrgdv  13357  subrgunit  13358  subrgpropd  13367  aprval  13370  islmod  13379  islmodd  13381  cncrng  13433  zsssubrg  13449  ntrval  13580  clsval  13581  cldcls  13584  neival  13613  resttop  13640  restco  13644  restabs  13645  resttopon2  13648  cnpval  13668  cnntr  13695  cnrest2  13706  upxp  13742  uptx  13744  cnmpt11  13753  cnmpt21  13761  psmetsym  13799  psmetres2  13803  xmetsym  13838  xmettxlem  13979  txmetcnp  13988  cnbl0  14004  cnblcld  14005  remetdval  14009  bl2ioo  14012  tgioo  14016  addcncntoplem  14021  divcnap  14025  fsumcncntop  14026  cncfmet  14049  cncfmptc  14052  addccncf  14056  negcncf  14058  mulcncflem  14060  ivthinclemlopn  14084  limcimolemlt  14103  cnplimcim  14106  cnplimclemr  14108  limccnp2lem  14115  limccnp2cntop  14116  dvfvalap  14120  dvconst  14131  dvaddxxbr  14135  dvmulxxbr  14136  dvcjbr  14142  dvexp  14145  dvrecap  14147  dvmptclx  14150  dvmptaddx  14151  dvmptmulx  14152  dvmptcmulcn  14153  dveflem  14157  dvef  14158  reeff1oleme  14163  sin0pilem1  14172  sin0pilem2  14173  efper  14198  sinperlem  14199  sinmpi  14206  cosmpi  14207  sinppi  14208  cosppi  14209  efimpi  14210  ptolemy  14215  sinq12gt0  14221  coseq0negpitopi  14227  tangtx  14229  abssinper  14237  cosq34lt1  14241  relogexp  14263  logdivlti  14272  logcxp  14288  rpcxp0  14289  rpcxp1  14290  1cxp  14291  ecxp  14292  rpcxpadd  14296  rpcxpp1  14297  rpmulcxp  14300  rpdivcxp  14302  cxpmul  14303  rpcxproot  14304  abscxp  14305  rpcxpsqrtth  14320  rplogbid1  14335  rplogb1  14336  rpelogb  14337  rplogbreexp  14341  rplogbzexp  14342  rprelogbmul  14343  rprelogbmulexp  14344  rprelogbdiv  14345  logbrec  14348  rpcxplogb  14352  logbgcd1irr  14355  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  binom4  14367  lgslem1  14371  lgsval2lem  14381  lgsvalmod  14390  lgsneg  14395  lgsdir2lem4  14402  lgsdirprm  14405  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgsmodeq  14416  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2lgsoddprmlem1  14423  2lgsoddprmlem2  14424  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  djucllem  14522  bj-charfun  14529  bj-charfundc  14530  bj-charfundcALT  14531  nninfsellemeq  14733  nninffeq  14739  qdencn  14745  cvgcmp2nlemabs  14750  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  apdifflemf  14764  redcwlpolemeq1  14772  dceqnconst  14777  dcapnconst  14778  nconstwlpolem0  14780  nconstwlpolemgt0  14781  nconstwlpolem  14782