Theorem eqtrd 2147

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

Syntax hints:   -> wi 4   = wceq 1314

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097

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

This theorem is referenced by:  eqtr2d  2148  eqtr3d  2149  eqtr4d  2150  3eqtrd  2151  3eqtrrd  2152  3eqtr2d  2153  syl5eq  2159  syl6eq  2163  rabeqbidv  2652  rabeqbidva  2653  csbidmg  3022  csbco3g  3024  difeq12d  3161  ifeq12d  3457  ifbieq1d  3460  ifbieq2d  3462  ifbieq12d  3464  eqifdc  3472  csbsng  3550  disjpr2  3553  csbunig  3710  iuneq12d  3803  unisn3  4326  op1stbg  4360  opthreg  4431  onsucuni2  4439  csbxpg  4580  coeq12d  4663  csbdmg  4693  reseq12d  4778  csbresg  4780  resima2  4811  imaeq12d  4840  csbrng  4958  opswapg  4983  relcnvtr  5016  relcoi2  5027  relcoi1  5028  iotaint  5059  funprg  5131  funtpg  5132  funcnvres2  5156  fnco  5189  fococnv2  5349  fveq12d  5382  csbfv12g  5411  csbfv2g  5412  csbfvg  5413  dffn5im  5421  funfvdm2  5439  fvun1  5441  fvmpt2d  5461  fvmptt  5466  fndmin  5481  fniniseg2  5496  fnniniseg2  5497  fmptcof  5541  fvresi  5567  fvunsng  5568  fvpr1g  5580  fvpr2g  5581  fvtp1g  5582  funiunfvdm  5618  fcof1o  5644  riotaeqbidv  5687  oveq123d  5749  csbov12g  5764  csbov1g  5765  csbov2g  5766  ovmpodxf  5850  caov42d  5911  caovdilemd  5916  caovimo  5918  grprinvd  5920  offeq  5949  offval2  5951  caofinvl  5958  ot1stg  6004  ot2ndg  6005  2nd1st  6032  mpomptsx  6049  dmmpossx  6051  fmpox  6052  fmpoco  6067  1stconst  6072  algrflemg  6081  tfrexlem  6185  rdgivallem  6232  rdgisuc1  6235  frec0g  6248  frecabcl  6250  frecsuclem  6257  frecrdg  6259  oa0  6307  oasuc  6314  oa1suc  6317  omsuc  6322  nnaass  6335  nndi  6336  nnmass  6337  nnm2  6375  nn2m  6376  ereq1  6390  errn  6405  uniqs2  6443  oviec  6489  ecovass  6492  ecoviass  6493  ecovdi  6494  ecovidi  6495  mapsnconst  6542  mapen  6693  mapxpen  6695  xpmapenlem  6696  phplem4on  6714  fidifsnen  6717  undifdc  6765  fiintim  6770  fisseneq  6773  snexxph  6790  sbthlemi4  6800  sbthlemi6  6802  supeq2  6828  eqsupti  6835  infvalti  6861  djuf1olem  6890  djuss  6907  1stinl  6911  2ndinl  6912  1stinr  6913  2ndinr  6914  updjudhcoinlf  6917  updjudhcoinrg  6918  omp1eomlem  6931  difinfsn  6937  ctmlemr  6945  ctssdclemn0  6947  ctssdc  6950  enumctlemm  6951  en2other2  7000  mulidpi  7074  addasspig  7086  mulasspig  7088  distrpig  7089  indpi  7098  addcmpblnq  7123  mulpipq  7128  dmaddpqlem  7133  nqpi  7134  addcomnqg  7137  recrecnq  7150  ltsonq  7154  ltanqg  7156  ltmnqg  7157  ltaddnq  7163  ltexnqq  7164  archnqq  7173  prarloclemarch  7174  ltrnqg  7176  ltnnnq  7179  nq0nn  7198  addcmpblnq0  7199  nqpnq0nq  7209  nqnq0a  7210  nq0m0r  7212  nq0a0  7213  distrnq0  7215  addassnq0  7218  nq02m  7221  prarloclemlo  7250  prarloclemcalc  7258  addnqprllem  7283  addnqprulem  7284  addnqprl  7285  addnqpru  7286  appdivnq  7319  mulnqprl  7324  mulnqpru  7325  addcanprlemu  7371  ltaprlem  7374  ltmprr  7398  cauappcvgprlemladdrl  7413  mulcmpblnrlemg  7483  mulcomsrg  7500  distrsrg  7502  ltsosr  7507  1idsr  7511  00sr  7512  ltasrg  7513  recexgt0sr  7516  srpospr  7525  prsradd  7528  prsrriota  7530  caucvgsrlemcau  7535  caucvgsrlemgt1  7537  caucvgsrlemoffval  7538  caucvgsrlemoffres  7542  caucvgsr  7544  elreal2  7565  mulresr  7573  pitonnlem1p1  7581  pitonnlem2  7582  pitoregt0  7584  recidpirqlemcalc  7592  recidpirq  7593  axaddcl  7599  axmulcl  7601  axmulcom  7606  axmulass  7608  axdistr  7609  ax1rid  7612  axcnre  7616  recriota  7625  axcaucvglemcau  7633  mulid1  7687  mulid2  7688  adddirp1d  7716  joinlmuladdmuld  7717  muladd11  7818  1p1times  7819  readdcan  7825  comraddd  7842  add42  7847  npcan  7894  addsubass  7895  2addsub  7899  addsubeq4  7900  nppcan  7907  nnpcan  7908  npncan2  7912  nncan  7914  subsub  7915  nnncan  7920  nnncan1  7921  pnpcan2  7925  pnncan  7926  subneg  7934  negneg  7935  negdi2  7943  mvrraddd  8049  subaddeqd  8050  addid0  8054  mul02  8068  mul01  8070  mulneg1  8076  mul2neg  8079  mulm1  8081  ltadd2  8100  rimul  8265  rereim  8266  mulreim  8284  recextlem1  8325  mulcanapd  8335  divcanap1  8354  divrecap2  8362  divmulassap  8368  divmulasscomap  8369  divcanap4  8372  dividap  8374  muldivdirap  8380  divdivdivap  8386  recdivap  8391  divadddivap  8400  divsubdivap  8401  div2negap  8408  divcanap5rd  8491  dmdcanap2d  8494  recgt0  8518  lt2mul2div  8547  nnmulcl  8651  times2  8753  add1p1  8873  sub1m1  8874  cnm2m1cnm3  8875  nn0supp  8933  peano2z  8994  nneoor  9057  supminfex  9294  cnref1o  9342  rexneg  9506  xaddpnf1  9522  xaddmnf1  9524  rexadd  9528  xaddid1  9538  xaddid2  9539  xaddass  9545  xpncan  9547  xleadd1a  9549  xltadd1  9552  xposdif  9558  xadd4d  9561  xleaddadd  9563  iooidg  9585  iooval2  9591  icoshftf1o  9667  lincmb01cmp  9679  iccf1o  9680  fzval2  9686  fzsuc  9742  fzpred  9743  fztpval  9756  fseq1p1m1  9767  fzshftral  9781  fzo0to3tp  9889  fzo0sn0fzo1  9891  fzosplitsn  9903  fzosplitprm1  9904  fzisfzounsn  9906  rebtwn2zlemstep  9923  2tnp1ge0ge0  9967  flqdiv  9987  modqvalr  9991  modqdiffl  10001  modqfrac  10003  modqmulnn  10008  modqid  10015  modqcyc  10025  modqcyc2  10026  mulp1mod1  10031  modqmuladd  10032  modqmuladdnn0  10034  qnegmod  10035  m1modnnsub1  10036  addmodid  10038  addmodidr  10039  modqmul12d  10044  modqnegd  10045  modqadd12d  10046  modifeq2int  10052  modqaddmulmod  10057  modqdi  10058  modqsubdir  10059  modsumfzodifsn  10062  addmodlteq  10064  frec2uzsucd  10067  frecuzrdgrrn  10074  frec2uzrdg  10075  frecuzrdglem  10077  frecuzrdgsuc  10080  frecuzrdgg  10082  frecuzrdgdomlem  10083  frecuzrdgfunlem  10085  frecuzrdgtclt  10087  frecuzrdgsuctlem  10089  frecfzennn  10092  seqeq1  10114  seq3val  10124  seqvalcd  10125  seq3p1  10128  seqp1cd  10132  seq3feq2  10136  seq3fveq  10137  seq3shft2  10139  seq3-1p  10146  iseqf1olemnab  10154  iseqf1olemab  10155  iseqf1olemnanb  10156  iseqf1olemqk  10160  iseqf1olemfvp  10163  seq3f1olemqsumkj  10164  seq3f1olemqsumk  10165  seq3f1olemqsum  10166  seq3f1o  10170  seq3id3  10173  seq3z  10177  fser0const  10182  exp3vallem  10187  expnnval  10189  expp1  10193  expn1ap0  10196  mulexp  10225  expaddzaplem  10229  expaddzap  10230  expmul  10231  expp1zap  10235  expm1ap  10236  sqval  10244  iexpcyc  10290  subsq2  10293  binom2  10296  binom21  10297  binom2sub1  10299  mulbinom2  10301  binom3  10302  zesq  10303  bernneq  10305  sqoddm1div8  10337  nn0opthlem1d  10359  facp1  10369  faclbnd6  10383  bcval2  10389  bcval3  10390  bcn0  10394  bcp1n  10400  bcp1nk  10401  bcn2  10403  bcp1m1  10404  bcpasc  10405  bcn2m1  10408  hashinfom  10417  hashennn  10419  hashfz1  10422  fseq1hash  10440  omgadd  10441  hashunsng  10446  hashprg  10447  hashdifsn  10458  hashdifpr  10459  hashfz  10460  hashfzo  10461  hashfzo0  10462  hashfzp1  10463  hashfz0  10464  hashxp  10465  resunimafz0  10467  fnfz0hash  10468  ffzo0hash  10470  hashfacen  10472  zfz1isolemsplit  10474  zfz1isolemiso  10475  zfz1isolem1  10476  shftdm  10487  shftval2  10491  shftval4  10493  shftval5  10494  shftcan1  10499  seq3shft  10503  imre  10516  crre  10522  remim  10525  reim0b  10527  recj  10532  reneg  10533  readd  10534  resub  10535  remullem  10536  imcj  10540  imneg  10541  imadd  10542  imsub  10543  cjcj  10548  cjadd  10549  ipcnval  10551  cjneg  10555  cjsub  10557  cjexp  10558  imval2  10559  cjap  10571  resqrexlemf1  10672  resqrexlemfp1  10673  resqrexlemover  10674  resqrexlemcalc1  10678  resqrexlemcalc3  10680  resqrexlemnm  10682  resqrexlemcvg  10683  resqrtcl  10693  sqrtsq  10708  absneg  10714  absvalsq  10717  absvalsq2  10718  sqabsadd  10719  sqabssub  10720  absval2  10721  absreimsq  10731  absmul  10733  absexp  10743  absexpzap  10744  abssuble0  10767  abstri  10768  recan  10773  amgm2  10782  maxabslemlub  10871  max0addsup  10883  minmax  10893  minabs  10899  bdtrilem  10902  bdtri  10903  xrmaxiflemab  10908  xrmaxiflemcom  10910  xrmaxadd  10922  xrminmax  10926  xrmineqinf  10930  xrminrecl  10934  xrbdtri  10937  climshft2  10967  subcn2  10972  reccn2ap  10974  climaddc2  10991  iser3shft  11007  climcvg1nlem  11010  sumeq12dv  11033  sumeq12rdv  11034  sumrbdclem  11037  fsum3cvg  11038  summodclem3  11041  summodclem2a  11042  summodc  11044  fsum3  11048  isumz  11050  fsumf1o  11051  fisumss  11053  fsumsersdc  11056  fsum3ser  11058  fsumsplit  11068  fsumsplitf  11069  sumsnf  11070  fsumsplitsn  11071  fsum1  11073  sumpr  11074  sumtp  11075  fsumm1  11077  fsum1p  11079  fsumsplitsnun  11080  fsump1  11081  isumclim  11082  sumnul  11085  isumadd  11092  fsum2dlemstep  11095  fsumcnv  11098  fisumcom2  11099  fsumshftm  11106  fisumrev2  11107  fisum0diag2  11108  fsumsub  11113  fsumdifsnconst  11116  modfsummodlemstep  11118  fsumabs  11126  telfsumo  11127  telfsum  11129  telfsum2  11130  fsumparts  11131  fsumiun  11138  hashiun  11139  hash2iun  11140  hash2iun1dif1  11141  binomlem  11144  binom1p  11146  binom11  11147  binom1dif  11148  bcxmas  11150  isum1p  11153  isumnn0nn  11154  isumlessdc  11157  divcnv  11158  arisum2  11160  trireciplem  11161  geosergap  11167  geolim  11172  georeclim  11174  geo2lim  11177  geoisum1  11180  cvgratnnlemnexp  11185  cvgratnnlemmn  11186  cvgratnnlemsumlt  11189  cvgratz  11193  mertenslemi1  11196  mertenslem2  11197  mertensabs  11198  eftabs  11213  efcllemp  11215  ef0lem  11217  efcvgfsum  11224  ege2le3  11228  efcj  11230  efaddlem  11231  efexp  11239  eftlub  11247  efsep  11248  effsumlt  11249  ef4p  11251  efgt1p2  11252  efgt1p  11253  tanval2ap  11271  tanval3ap  11272  resinval  11273  recosval  11274  efi4p  11275  resin4p  11276  recos4p  11277  sinneg  11284  cosneg  11285  tannegap  11286  efmival  11291  sinadd  11294  cosadd  11295  tanaddaplem  11296  tanaddap  11297  sinsub  11298  cossub  11299  addsin  11300  subsin  11301  subcos  11305  sincossq  11306  sin2t  11307  sin01bnd  11315  cos01bnd  11316  absefi  11325  absef  11326  absefib  11327  efieq1re  11328  demoivre  11329  demoivreALT  11330  eirraplem  11331  dvdstr  11378  dvdsadd2b  11388  mulmoddvds  11409  ltoddhalfle  11438  opoe  11440  m1expo  11445  m1exp1  11446  flodddiv4  11479  flodddiv4t2lthalf  11482  zsupcllemstep  11486  nn0gcdid0  11517  gcdaddm  11520  gcdadd  11521  gcdid  11522  gcdabs  11524  modgcd  11527  1gcd  11528  bezout  11545  dfgcd2  11548  mulgcd  11550  absmulgcd  11551  gcdmultiple  11554  gcdmultiplez  11555  rpmulgcd  11560  rplpwr  11561  rppwr  11562  dvdssqlem  11564  ialgr0  11571  alginv  11574  algcvg  11575  algfx  11579  eucalginv  11583  eucalglt  11584  lcmcl  11599  lcmabs  11603  lcmgcdlem  11604  lcmdvds  11606  lcmgcdnn  11609  coprmdvds  11619  qredeq  11623  divgcdcoprm0  11628  divgcdcoprmex  11629  rpexp1i  11678  sqrt2irrlem  11685  sqpweven  11698  2sqpwodd  11699  sqrt2irraplemnn  11702  qmuldeneqnum  11718  nn0gcdsq  11723  numdensq  11725  nn0sqrtelqelz  11729  phibndlem  11737  dfphi2  11741  phiprmpw  11743  phiprm  11744  phimullem  11746  hashgcdlem  11748  ennnfonelemp1  11764  ennnfonelemhdmp1  11767  ennnfonelemss  11768  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemhom  11773  ennnfonelemnn0  11780  ctinfomlemom  11785  setsvala  11833  fvsetsid  11836  setsresg  11840  setscom  11842  setsslid  11852  ressid2  11861  ressval2  11862  restid2  11972  ntrval  12122  clsval  12123  cldcls  12126  neival  12155  resttop  12182  restco  12186  restabs  12187  resttopon2  12190  cnpval  12209  cnntr  12236  cnrest2  12247  upxp  12283  uptx  12285  cnmpt11  12294  cnmpt21  12302  psmetsym  12318  psmetres2  12322  xmetsym  12357  xmettxlem  12498  txmetcnp  12507  cnbl0  12523  cnblcld  12524  remetdval  12525  bl2ioo  12528  tgioo  12532  addcncntoplem  12537  divcnap  12541  fsumcncntop  12542  cncfmet  12565  cncfmptc  12568  addccncf  12572  negcncf  12574  mulcncflem  12576  limcimolemlt  12589  cnplimcim  12592  cnplimclemr  12594  limccnp2lem  12601  limccnp2cntop  12602  dvfvalap  12605  dvconst  12616  dvaddxxbr  12620  dvmulxxbr  12621  djucllem  12699  nninfalllemn  12894  nninfsellemeq  12902  nninffeq  12908  qdencn  12914  cvgcmp2nlemabs  12919  trilpolemisumle  12923  trilpolemeq1  12925  trilpolemlt1  12926