Theorem eqtrd 2170

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

Syntax hints:   -> wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  eqtr2d  2171  eqtr3d  2172  eqtr4d  2173  3eqtrd  2174  3eqtrrd  2175  3eqtr2d  2176  syl5eq  2182  syl6eq  2186  rabeqbidv  2676  rabeqbidva  2677  csbidmg  3051  csbco3g  3053  difeq12d  3190  ifeq12d  3486  ifbieq1d  3489  ifbieq2d  3491  ifbieq12d  3493  eqifdc  3501  csbsng  3579  disjpr2  3582  csbunig  3739  iuneq12d  3832  unisn3  4361  op1stbg  4395  opthreg  4466  onsucuni2  4474  csbxpg  4615  coeq12d  4698  csbdmg  4728  reseq12d  4815  csbresg  4817  resima2  4848  imaeq12d  4877  csbrng  4995  opswapg  5020  relcnvtr  5053  relcoi2  5064  relcoi1  5065  iotaint  5096  funprg  5168  funtpg  5169  funcnvres2  5193  fnco  5226  fococnv2  5386  fveq12d  5421  csbfv12g  5450  csbfv2g  5451  csbfvg  5452  dffn5im  5460  funfvdm2  5478  fvun1  5480  fvmpt2d  5500  fvmptt  5505  fndmin  5520  fniniseg2  5535  fnniniseg2  5536  fmptcof  5580  fvresi  5606  fvunsng  5607  fvpr1g  5619  fvpr2g  5620  fvtp1g  5621  funiunfvdm  5657  fcof1o  5683  riotaeqbidv  5726  oveq123d  5788  csbov12g  5803  csbov1g  5804  csbov2g  5805  ovmpodxf  5889  caov42d  5950  caovdilemd  5955  caovimo  5957  grprinvd  5959  offeq  5988  offval2  5990  caofinvl  5997  ot1stg  6043  ot2ndg  6044  2nd1st  6071  mpomptsx  6088  dmmpossx  6090  fmpox  6091  fmpoco  6106  1stconst  6111  algrflemg  6120  tfrexlem  6224  rdgivallem  6271  rdgisuc1  6274  frec0g  6287  frecabcl  6289  frecsuclem  6296  frecrdg  6298  oa0  6346  oasuc  6353  oa1suc  6356  omsuc  6361  nnaass  6374  nndi  6375  nnmass  6376  nnm2  6414  nn2m  6415  ereq1  6429  errn  6444  uniqs2  6482  oviec  6528  ecovass  6531  ecoviass  6532  ecovdi  6533  ecovidi  6534  mapsnconst  6581  mapen  6733  mapxpen  6735  xpmapenlem  6736  phplem4on  6754  fidifsnen  6757  undifdc  6805  fiintim  6810  fisseneq  6813  snexxph  6831  sbthlemi4  6841  sbthlemi6  6843  supeq2  6869  eqsupti  6876  infvalti  6902  djuf1olem  6931  djuss  6948  1stinl  6952  2ndinl  6953  1stinr  6954  2ndinr  6955  updjudhcoinlf  6958  updjudhcoinrg  6959  omp1eomlem  6972  difinfsn  6978  ctmlemr  6986  ctssdclemn0  6988  ctssdc  6991  enumctlemm  6992  en2other2  7045  mulidpi  7119  addasspig  7131  mulasspig  7133  distrpig  7134  indpi  7143  addcmpblnq  7168  mulpipq  7173  dmaddpqlem  7178  nqpi  7179  addcomnqg  7182  recrecnq  7195  ltsonq  7199  ltanqg  7201  ltmnqg  7202  ltaddnq  7208  ltexnqq  7209  archnqq  7218  prarloclemarch  7219  ltrnqg  7221  ltnnnq  7224  nq0nn  7243  addcmpblnq0  7244  nqpnq0nq  7254  nqnq0a  7255  nq0m0r  7257  nq0a0  7258  distrnq0  7260  addassnq0  7263  nq02m  7266  prarloclemlo  7295  prarloclemcalc  7303  addnqprllem  7328  addnqprulem  7329  addnqprl  7330  addnqpru  7331  appdivnq  7364  mulnqprl  7369  mulnqpru  7370  addcanprlemu  7416  ltaprlem  7419  ltmprr  7443  cauappcvgprlemladdrl  7458  mulcmpblnrlemg  7541  mulcomsrg  7558  distrsrg  7560  ltsosr  7565  1idsr  7569  00sr  7570  ltasrg  7571  recexgt0sr  7574  srpospr  7584  prsradd  7587  prsrriota  7589  caucvgsrlemcau  7594  caucvgsrlemgt1  7596  caucvgsrlemoffval  7597  caucvgsrlemoffres  7601  caucvgsr  7603  map2psrprg  7606  elreal2  7631  mulresr  7639  pitonnlem1p1  7647  pitonnlem2  7648  pitoregt0  7650  recidpirqlemcalc  7658  recidpirq  7659  axaddcl  7665  axmulcl  7667  axmulcom  7672  axmulass  7674  axdistr  7675  ax1rid  7678  axcnre  7682  recriota  7691  axcaucvglemcau  7699  mulid1  7756  mulid2  7757  adddirp1d  7785  joinlmuladdmuld  7786  muladd11  7888  1p1times  7889  readdcan  7895  comraddd  7912  add42  7917  npcan  7964  addsubass  7965  2addsub  7969  addsubeq4  7970  nppcan  7977  nnpcan  7978  npncan2  7982  nncan  7984  subsub  7985  nnncan  7990  nnncan1  7991  pnpcan2  7995  pnncan  7996  subneg  8004  negneg  8005  negdi2  8013  mvrraddd  8121  assraddsubd  8123  subaddeqd  8124  addid0  8128  mul02  8142  mul01  8144  mulneg1  8150  mul2neg  8153  mulm1  8155  ltadd2  8174  rimul  8340  rereim  8341  mulreim  8359  recextlem1  8405  mulcanapd  8415  divcanap1  8434  divrecap2  8442  divmulassap  8448  divmulasscomap  8449  divcanap4  8452  dividap  8454  muldivdirap  8460  divdivdivap  8466  recdivap  8471  divadddivap  8480  divsubdivap  8481  div2negap  8488  divcanap5rd  8571  dmdcanap2d  8574  subrecap  8591  recgt0  8601  lt2mul2div  8630  nnmulcl  8734  times2  8842  add1p1  8962  sub1m1  8963  cnm2m1cnm3  8964  nn0supp  9022  peano2z  9083  nneoor  9146  supminfex  9385  cnref1o  9433  rexneg  9606  xaddpnf1  9622  xaddmnf1  9624  rexadd  9628  xaddid1  9638  xaddid2  9639  xaddass  9645  xpncan  9647  xleadd1a  9649  xltadd1  9652  xposdif  9658  xadd4d  9661  xleaddadd  9663  iooidg  9685  iooval2  9691  icoshftf1o  9767  lincmb01cmp  9779  iccf1o  9780  fzval2  9786  fzsuc  9842  fzpred  9843  fztpval  9856  fseq1p1m1  9867  fzshftral  9881  fzo0to3tp  9989  fzo0sn0fzo1  9991  fzosplitsn  10003  fzosplitprm1  10004  fzisfzounsn  10006  rebtwn2zlemstep  10023  2tnp1ge0ge0  10067  flqdiv  10087  modqvalr  10091  modqdiffl  10101  modqfrac  10103  modqmulnn  10108  modqid  10115  modqcyc  10125  modqcyc2  10126  mulp1mod1  10131  modqmuladd  10132  modqmuladdnn0  10134  qnegmod  10135  m1modnnsub1  10136  addmodid  10138  addmodidr  10139  modqmul12d  10144  modqnegd  10145  modqadd12d  10146  modifeq2int  10152  modqaddmulmod  10157  modqdi  10158  modqsubdir  10159  modsumfzodifsn  10162  addmodlteq  10164  frec2uzsucd  10167  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdglem  10177  frecuzrdgsuc  10180  frecuzrdgg  10182  frecuzrdgdomlem  10183  frecuzrdgfunlem  10185  frecuzrdgtclt  10187  frecuzrdgsuctlem  10189  frecfzennn  10192  seqeq1  10214  seq3val  10224  seqvalcd  10225  seq3p1  10228  seqp1cd  10232  seq3feq2  10236  seq3fveq  10237  seq3shft2  10239  seq3-1p  10246  iseqf1olemnab  10254  iseqf1olemab  10255  iseqf1olemnanb  10256  iseqf1olemqk  10260  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1o  10270  seq3id3  10273  seq3z  10277  fser0const  10282  exp3vallem  10287  expnnval  10289  expp1  10293  expn1ap0  10296  mulexp  10325  expaddzaplem  10329  expaddzap  10330  expmul  10331  expp1zap  10335  expm1ap  10336  sqval  10344  iexpcyc  10390  subsq2  10393  binom2  10396  binom21  10397  binom2sub1  10399  mulbinom2  10401  binom3  10402  zesq  10403  bernneq  10405  sqoddm1div8  10437  nn0opthlem1d  10459  facp1  10469  faclbnd6  10483  bcval2  10489  bcval3  10490  bcn0  10494  bcp1n  10500  bcp1nk  10501  bcn2  10503  bcp1m1  10504  bcpasc  10505  bcn2m1  10508  hashinfom  10517  hashennn  10519  hashfz1  10522  fseq1hash  10540  omgadd  10541  hashunsng  10546  hashprg  10547  hashdifsn  10558  hashdifpr  10559  hashfz  10560  hashfzo  10561  hashfzo0  10562  hashfzp1  10563  hashfz0  10564  hashxp  10565  resunimafz0  10567  fnfz0hash  10568  ffzo0hash  10570  hashfacen  10572  zfz1isolemsplit  10574  zfz1isolemiso  10575  zfz1isolem1  10576  shftdm  10587  shftval2  10591  shftval4  10593  shftval5  10594  shftcan1  10599  seq3shft  10603  imre  10616  crre  10622  remim  10625  reim0b  10627  recj  10632  reneg  10633  readd  10634  resub  10635  remullem  10636  imcj  10640  imneg  10641  imadd  10642  imsub  10643  cjcj  10648  cjadd  10649  ipcnval  10651  cjneg  10655  cjsub  10657  cjexp  10658  imval2  10659  cjap  10671  resqrexlemf1  10773  resqrexlemfp1  10774  resqrexlemover  10775  resqrexlemcalc1  10779  resqrexlemcalc3  10781  resqrexlemnm  10783  resqrexlemcvg  10784  resqrtcl  10794  sqrtsq  10809  absneg  10815  absvalsq  10818  absvalsq2  10819  sqabsadd  10820  sqabssub  10821  absval2  10822  absreimsq  10832  absmul  10834  absexp  10844  absexpzap  10845  abssuble0  10868  abstri  10869  recan  10874  amgm2  10883  maxabslemlub  10972  max0addsup  10984  minmax  10994  minabs  11000  bdtrilem  11003  bdtri  11004  xrmaxiflemab  11009  xrmaxiflemcom  11011  xrmaxadd  11023  xrminmax  11027  xrmineqinf  11031  xrminrecl  11035  xrbdtri  11038  climshft2  11068  subcn2  11073  reccn2ap  11075  climaddc2  11092  iser3shft  11108  climcvg1nlem  11111  sumeq12dv  11134  sumeq12rdv  11135  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  summodc  11145  fsum3  11149  isumz  11151  fsumf1o  11152  fisumss  11154  fsumsersdc  11157  fsum3ser  11159  fsumsplit  11169  fsumsplitf  11170  sumsnf  11171  fsumsplitsn  11172  fsum1  11174  sumpr  11175  sumtp  11176  fsumm1  11178  fsum1p  11180  fsumsplitsnun  11181  fsump1  11182  isumclim  11183  sumnul  11186  isumadd  11193  fsum2dlemstep  11196  fsumcnv  11199  fisumcom2  11200  fsumshftm  11207  fisumrev2  11208  fisum0diag2  11209  fsumsub  11214  fsumdifsnconst  11217  modfsummodlemstep  11219  fsumabs  11227  telfsumo  11228  telfsum  11230  telfsum2  11231  fsumparts  11232  fsumiun  11239  hashiun  11240  hash2iun  11241  hash2iun1dif1  11242  binomlem  11245  binom1p  11247  binom11  11248  binom1dif  11249  bcxmas  11251  isum1p  11254  isumnn0nn  11255  isumlessdc  11258  divcnv  11259  arisum2  11261  trireciplem  11262  geosergap  11268  geolim  11273  georeclim  11275  geo2lim  11278  geoisum1  11281  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemsumlt  11290  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodfrecap  11308  prodeq12dv  11331  prodeq12rdv  11332  prodrbdclem  11333  fproddccvg  11334  eftabs  11351  efcllemp  11353  ef0lem  11355  efcvgfsum  11362  ege2le3  11366  efcj  11368  efaddlem  11369  efexp  11377  eftlub  11385  efsep  11386  effsumlt  11387  ef4p  11389  efgt1p2  11390  efgt1p  11391  tanval2ap  11409  tanval3ap  11410  resinval  11411  recosval  11412  efi4p  11413  resin4p  11414  recos4p  11415  sinneg  11422  cosneg  11423  tannegap  11424  efmival  11429  sinadd  11432  cosadd  11433  tanaddaplem  11434  tanaddap  11435  sinsub  11436  cossub  11437  addsin  11438  subsin  11439  subcos  11443  sincossq  11444  sin2t  11445  sin01bnd  11453  cos01bnd  11454  absefi  11464  absef  11465  absefib  11466  efieq1re  11467  demoivre  11468  demoivreALT  11469  eirraplem  11472  dvdstr  11519  dvdsadd2b  11529  mulmoddvds  11550  ltoddhalfle  11579  opoe  11581  m1expo  11586  m1exp1  11587  flodddiv4  11620  flodddiv4t2lthalf  11623  zsupcllemstep  11627  nn0gcdid0  11658  gcdaddm  11661  gcdadd  11662  gcdid  11663  gcdabs  11665  modgcd  11668  1gcd  11669  bezout  11688  dfgcd2  11691  mulgcd  11693  absmulgcd  11694  gcdmultiple  11697  gcdmultiplez  11698  rpmulgcd  11703  rplpwr  11704  rppwr  11705  dvdssqlem  11707  ialgr0  11714  alginv  11717  algcvg  11718  algfx  11722  eucalginv  11726  eucalglt  11727  lcmcl  11742  lcmabs  11746  lcmgcdlem  11747  lcmdvds  11749  lcmgcdnn  11752  coprmdvds  11762  qredeq  11766  divgcdcoprm0  11771  divgcdcoprmex  11772  rpexp1i  11821  sqrt2irrlem  11828  sqpweven  11842  2sqpwodd  11843  sqrt2irraplemnn  11846  qmuldeneqnum  11862  nn0gcdsq  11867  numdensq  11869  nn0sqrtelqelz  11873  phibndlem  11881  dfphi2  11885  phiprmpw  11887  phiprm  11888  phimullem  11890  hashgcdlem  11892  ennnfonelemp1  11908  ennnfonelemhdmp1  11911  ennnfonelemss  11912  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  ennnfonelemnn0  11924  ctinfomlemom  11929  setsvala  11979  fvsetsid  11982  setsresg  11986  setscom  11988  setsslid  11998  ressid2  12007  ressval2  12008  restid2  12118  ntrval  12268  clsval  12269  cldcls  12272  neival  12301  resttop  12328  restco  12332  restabs  12333  resttopon2  12336  cnpval  12356  cnntr  12383  cnrest2  12394  upxp  12430  uptx  12432  cnmpt11  12441  cnmpt21  12449  psmetsym  12487  psmetres2  12491  xmetsym  12526  xmettxlem  12667  txmetcnp  12676  cnbl0  12692  cnblcld  12693  remetdval  12697  bl2ioo  12700  tgioo  12704  addcncntoplem  12709  divcnap  12713  fsumcncntop  12714  cncfmet  12737  cncfmptc  12740  addccncf  12744  negcncf  12746  mulcncflem  12748  ivthinclemlopn  12772  limcimolemlt  12791  cnplimcim  12794  cnplimclemr  12796  limccnp2lem  12803  limccnp2cntop  12804  dvfvalap  12808  dvconst  12819  dvaddxxbr  12823  dvmulxxbr  12824  dvcjbr  12830  dvexp  12833  dvrecap  12835  dvmptclx  12838  dvmptaddx  12839  dvmptmulx  12840  dvmptcmulcn  12841  dveflem  12844  dvef  12845  sin0pilem1  12851  sin0pilem2  12852  efper  12877  sinperlem  12878  sinmpi  12885  cosmpi  12886  sinppi  12887  cosppi  12888  efimpi  12889  ptolemy  12894  sinq12gt0  12900  coseq0negpitopi  12906  tangtx  12908  abssinper  12916  cosq34lt1  12920  djucllem  12996  nninfalllemn  13191  nninfsellemeq  13199  nninffeq  13205  qdencn  13211  cvgcmp2nlemabs  13216  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223