Theorem eqtrd 2197

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtrd	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrd

Step	Hyp	Ref	Expression
1		eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eqeq2d 2176	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1342

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 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

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

This theorem is referenced by:  eqtr2d  2198  eqtr3d  2199  eqtr4d  2200  3eqtrd  2201  3eqtrrd  2202  3eqtr2d  2203  syl5eq  2209  eqtrdi  2213  rabeqbidv  2716  rabeqbidva  2717  csbidmg  3096  csbco3g  3098  difeq12d  3236  ifeq12d  3534  ifbieq1d  3537  ifbieq2d  3539  ifbieq12d  3541  eqifdc  3549  csbsng  3631  disjpr2  3634  csbunig  3791  iuneq12d  3884  unisn3  4417  op1stbg  4451  opthreg  4527  onsucuni2  4535  csbxpg  4679  coeq12d  4762  csbdmg  4792  reseq12d  4879  csbresg  4881  resima2  4912  imaeq12d  4941  csbrng  5059  opswapg  5084  relcnvtr  5117  relcoi2  5128  relcoi1  5129  iotaint  5160  funprg  5232  funtpg  5233  funcnvres2  5257  fnco  5290  fococnv2  5452  fveq12d  5487  csbfv12g  5516  csbfv2g  5517  csbfvg  5518  dffn5im  5526  funfvdm2  5544  fvun1  5546  fvmpt2d  5566  fvmptt  5571  fndmin  5586  fniniseg2  5601  fnniniseg2  5602  fmptcof  5646  fvresi  5672  fvunsng  5673  fvpr1g  5685  fvpr2g  5686  fvtp1g  5687  funiunfvdm  5725  fcof1o  5751  riotaeqbidv  5795  oveq123d  5857  csbov12g  5872  csbov1g  5873  csbov2g  5874  ovmpodxf  5958  caov42d  6019  caovdilemd  6024  caovimo  6026  grprinvd  6028  offeq  6057  offval2  6059  caofinvl  6066  ot1stg  6112  ot2ndg  6113  2nd1st  6140  mpomptsx  6157  dmmpossx  6159  fmpox  6160  fmpoco  6175  1stconst  6180  algrflemg  6189  tfrexlem  6293  rdgivallem  6340  rdgisuc1  6343  frec0g  6356  frecabcl  6358  frecsuclem  6365  frecrdg  6367  oa0  6416  oasuc  6423  oa1suc  6426  omsuc  6431  nnaass  6444  nndi  6445  nnmass  6446  nnm2  6484  nn2m  6485  ereq1  6499  errn  6514  uniqs2  6552  oviec  6598  ecovass  6601  ecoviass  6602  ecovdi  6603  ecovidi  6604  mapsnconst  6651  mapen  6803  mapxpen  6805  xpmapenlem  6806  phplem4on  6824  fidifsnen  6827  undifdc  6880  fiintim  6885  fisseneq  6888  snexxph  6906  sbthlemi4  6916  sbthlemi6  6918  supeq2  6945  eqsupti  6952  infvalti  6978  djuf1olem  7009  djuss  7026  1stinl  7030  2ndinl  7031  1stinr  7032  2ndinr  7033  updjudhcoinlf  7036  updjudhcoinrg  7037  omp1eomlem  7050  difinfsn  7056  ctmlemr  7064  ctssdclemn0  7066  ctssdc  7069  enumctlemm  7070  nnnninfeq  7083  nnnninfeq2  7084  nninfisollemne  7086  nninfisol  7088  enwomnilem  7124  en2other2  7143  cc3  7200  mulidpi  7250  addasspig  7262  mulasspig  7264  distrpig  7265  indpi  7274  addcmpblnq  7299  mulpipq  7304  dmaddpqlem  7309  nqpi  7310  addcomnqg  7313  recrecnq  7326  ltsonq  7330  ltanqg  7332  ltmnqg  7333  ltaddnq  7339  ltexnqq  7340  archnqq  7349  prarloclemarch  7350  ltrnqg  7352  ltnnnq  7355  nq0nn  7374  addcmpblnq0  7375  nqpnq0nq  7385  nqnq0a  7386  nq0m0r  7388  nq0a0  7389  distrnq0  7391  addassnq0  7394  nq02m  7397  prarloclemlo  7426  prarloclemcalc  7434  addnqprllem  7459  addnqprulem  7460  addnqprl  7461  addnqpru  7462  appdivnq  7495  mulnqprl  7500  mulnqpru  7501  addcanprlemu  7547  ltaprlem  7550  ltmprr  7574  cauappcvgprlemladdrl  7589  mulcmpblnrlemg  7672  mulcomsrg  7689  distrsrg  7691  ltsosr  7696  1idsr  7700  00sr  7701  ltasrg  7702  recexgt0sr  7705  srpospr  7715  prsradd  7718  prsrriota  7720  caucvgsrlemcau  7725  caucvgsrlemgt1  7727  caucvgsrlemoffval  7728  caucvgsrlemoffres  7732  caucvgsr  7734  map2psrprg  7737  elreal2  7762  mulresr  7770  pitonnlem1p1  7778  pitonnlem2  7779  pitoregt0  7781  recidpirqlemcalc  7789  recidpirq  7790  axaddcl  7796  axmulcl  7798  axmulcom  7803  axmulass  7805  axdistr  7806  ax1rid  7809  axcnre  7813  recriota  7822  axcaucvglemcau  7830  mulid1  7887  mulid2  7888  adddirp1d  7916  joinlmuladdmuld  7917  muladd11  8022  1p1times  8023  readdcan  8029  comraddd  8046  add42  8051  npcan  8098  addsubass  8099  2addsub  8103  addsubeq4  8104  nppcan  8111  nnpcan  8112  npncan2  8116  nncan  8118  subsub  8119  nnncan  8124  nnncan1  8125  pnpcan2  8129  pnncan  8130  subneg  8138  negneg  8139  negdi2  8147  mvrraddd  8255  assraddsubd  8257  subaddeqd  8258  addid0  8262  mul02  8276  mul01  8278  mulneg1  8284  mul2neg  8287  mulm1  8289  ltadd2  8308  rimul  8474  rereim  8475  mulreim  8493  recextlem1  8539  mulcanapd  8549  divcanap1  8568  divrecap2  8576  divmulassap  8582  divmulasscomap  8583  divcanap4  8586  dividap  8588  muldivdirap  8594  divdivdivap  8600  recdivap  8605  divadddivap  8614  divsubdivap  8615  div2negap  8622  divcanap5rd  8705  dmdcanap2d  8708  subrecap  8726  recgt0  8736  lt2mul2div  8765  nnmulcl  8869  times2  8977  add1p1  9097  sub1m1  9098  cnm2m1cnm3  9099  nn0supp  9157  peano2z  9218  nneoor  9284  supminfex  9526  cnref1o  9579  rexneg  9757  xaddpnf1  9773  xaddmnf1  9775  rexadd  9779  xaddid1  9789  xaddid2  9790  xaddass  9796  xpncan  9798  xleadd1a  9800  xltadd1  9803  xposdif  9809  xadd4d  9812  xleaddadd  9814  iooidg  9836  iooval2  9842  icoshftf1o  9918  lincmb01cmp  9930  iccf1o  9931  fzval2  9938  fzsuc  9994  fzpred  9995  fztpval  10008  fseq1p1m1  10019  fzshftral  10033  fz0to4untppr  10049  fzo0to3tp  10144  fzo0sn0fzo1  10146  fzosplitsn  10158  fzosplitprm1  10159  fzisfzounsn  10161  rebtwn2zlemstep  10178  2tnp1ge0ge0  10226  flqdiv  10246  modqvalr  10250  modqdiffl  10260  modqfrac  10262  modqmulnn  10267  modqid  10274  modqcyc  10284  modqcyc2  10285  mulp1mod1  10290  modqmuladd  10291  modqmuladdnn0  10293  qnegmod  10294  m1modnnsub1  10295  addmodid  10297  addmodidr  10298  modqmul12d  10303  modqnegd  10304  modqadd12d  10305  modifeq2int  10311  modqaddmulmod  10316  modqdi  10317  modqsubdir  10318  modsumfzodifsn  10321  addmodlteq  10323  frec2uzsucd  10326  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdglem  10336  frecuzrdgsuc  10339  frecuzrdgg  10341  frecuzrdgdomlem  10342  frecuzrdgfunlem  10344  frecuzrdgtclt  10346  frecuzrdgsuctlem  10348  frecfzennn  10351  seqeq1  10373  seq3val  10383  seqvalcd  10384  seq3p1  10387  seqp1cd  10391  seq3feq2  10395  seq3fveq  10396  seq3shft2  10398  seq3-1p  10405  iseqf1olemnab  10413  iseqf1olemab  10414  iseqf1olemnanb  10415  iseqf1olemqk  10419  iseqf1olemfvp  10422  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3f1o  10429  seq3id3  10432  seq3z  10436  fser0const  10441  exp3vallem  10446  expnnval  10448  expp1  10452  expn1ap0  10455  mulexp  10484  expaddzaplem  10488  expaddzap  10489  expmul  10490  expp1zap  10494  expm1ap  10495  sqval  10503  iexpcyc  10549  subsq2  10552  binom2  10555  binom21  10556  binom2sub1  10558  mulbinom2  10560  binom3  10561  zesq  10562  bernneq  10564  sqoddm1div8  10597  nn0opthlem1d  10622  facp1  10632  faclbnd6  10646  bcval2  10652  bcval3  10653  bcn0  10657  bcp1n  10663  bcp1nk  10664  bcn2  10666  bcp1m1  10667  bcpasc  10668  bcn2m1  10671  hashinfom  10680  hashennn  10682  hashfz1  10685  fseq1hash  10703  omgadd  10704  hashunsng  10709  hashprg  10710  hashdifsn  10721  hashdifpr  10722  hashfz  10723  hashfzo  10724  hashfzo0  10725  hashfzp1  10726  hashfz0  10727  hashxp  10728  resunimafz0  10730  fnfz0hash  10731  ffzo0hash  10733  hashfacen  10735  zfz1isolemsplit  10737  zfz1isolemiso  10738  zfz1isolem1  10739  shftdm  10750  shftval2  10754  shftval4  10756  shftval5  10757  shftcan1  10762  seq3shft  10766  imre  10779  crre  10785  remim  10788  reim0b  10790  recj  10795  reneg  10796  readd  10797  resub  10798  remullem  10799  imcj  10803  imneg  10804  imadd  10805  imsub  10806  cjcj  10811  cjadd  10812  ipcnval  10814  cjneg  10818  cjsub  10820  cjexp  10821  imval2  10822  cjap  10834  resqrexlemf1  10936  resqrexlemfp1  10937  resqrexlemover  10938  resqrexlemcalc1  10942  resqrexlemcalc3  10944  resqrexlemnm  10946  resqrexlemcvg  10947  resqrtcl  10957  sqrtsq  10972  absneg  10978  absvalsq  10981  absvalsq2  10982  sqabsadd  10983  sqabssub  10984  absval2  10985  absreimsq  10995  absmul  10997  absexp  11007  absexpzap  11008  abssuble0  11031  abstri  11032  recan  11037  amgm2  11046  maxabslemlub  11135  max0addsup  11147  minmax  11157  minabs  11163  bdtrilem  11166  bdtri  11167  xrmaxiflemab  11174  xrmaxiflemcom  11176  xrmaxadd  11188  xrminmax  11192  xrmineqinf  11196  xrminrecl  11200  xrbdtri  11203  climshft2  11233  subcn2  11238  reccn2ap  11240  climaddc2  11257  iser3shft  11273  climcvg1nlem  11276  sumeq12dv  11299  sumeq12rdv  11300  sumrbdclem  11304  fsum3cvg  11305  summodclem3  11307  summodclem2a  11308  summodc  11310  fsum3  11314  isumz  11316  fsumf1o  11317  fisumss  11319  fsumsersdc  11322  fsum3ser  11324  fsumsplit  11334  fsumsplitf  11335  sumsnf  11336  fsumsplitsn  11337  fsum1  11339  sumpr  11340  sumtp  11341  fsumm1  11343  fsum1p  11345  fsumsplitsnun  11346  fsump1  11347  isumclim  11348  sumnul  11351  isumadd  11358  fsum2dlemstep  11361  fsumcnv  11364  fisumcom2  11365  fsumshftm  11372  fisumrev2  11373  fisum0diag2  11374  fsumsub  11379  fsumdifsnconst  11382  modfsummodlemstep  11384  fsumabs  11392  telfsumo  11393  telfsum  11395  telfsum2  11396  fsumparts  11397  fsumiun  11404  hashiun  11405  hash2iun  11406  hash2iun1dif1  11407  binomlem  11410  binom1p  11412  binom11  11413  binom1dif  11414  bcxmas  11416  isum1p  11419  isumnn0nn  11420  isumlessdc  11423  divcnv  11424  arisum2  11426  trireciplem  11427  geosergap  11433  geolim  11438  georeclim  11440  geo2lim  11443  geoisum1  11446  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemsumlt  11455  cvgratz  11459  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  prodfrecap  11473  prodeq12dv  11496  prodeq12rdv  11497  prodrbdclem  11498  fproddccvg  11499  prodmodclem3  11502  prodmodclem2a  11503  zprodap0  11508  fprodseq  11510  fprodntrivap  11511  prod1dc  11513  fprodf1o  11515  prodssdc  11516  fprodssdc  11517  prodsnf  11519  fprod1  11521  fprodsplitdc  11523  fprodm1  11525  fprod1p  11526  fprodp1  11527  fprodunsn  11531  fprodcl2lem  11532  fprodabs  11543  fprodconst  11547  fprod2dlemstep  11549  fprodcnv  11552  fprodcom2fi  11553  fprodrec  11556  fprodsplitsn  11560  fprodsplit1f  11561  fprodeq0g  11565  eftabs  11583  efcllemp  11585  ef0lem  11587  efcvgfsum  11594  ege2le3  11598  efcj  11600  efaddlem  11601  efexp  11609  eftlub  11617  efsep  11618  effsumlt  11619  ef4p  11621  efgt1p2  11622  efgt1p  11623  tanval2ap  11640  tanval3ap  11641  resinval  11642  recosval  11643  efi4p  11644  resin4p  11645  recos4p  11646  sinneg  11653  cosneg  11654  tannegap  11655  efmival  11660  sinadd  11663  cosadd  11664  tanaddaplem  11665  tanaddap  11666  sinsub  11667  cossub  11668  addsin  11669  subsin  11670  subcos  11674  sincossq  11675  sin2t  11676  sin01bnd  11684  cos01bnd  11685  absefi  11695  absef  11696  absefib  11697  efieq1re  11698  demoivre  11699  demoivreALT  11700  eirraplem  11703  dvdstr  11754  dvdsadd2b  11765  mulmoddvds  11786  ltoddhalfle  11815  opoe  11817  m1expo  11822  m1exp1  11823  flodddiv4  11856  flodddiv4t2lthalf  11859  zsupcllemstep  11863  nn0gcdid0  11899  gcdaddm  11902  gcdadd  11903  gcdid  11904  gcdabs  11906  modgcd  11909  1gcd  11910  bezout  11929  dfgcd2  11932  mulgcd  11934  absmulgcd  11935  gcdmultiple  11938  gcdmultiplez  11939  rpmulgcd  11944  rplpwr  11945  rppwr  11946  dvdssqlem  11948  ialgr0  11955  alginv  11958  algcvg  11959  algfx  11963  eucalginv  11967  eucalglt  11968  lcmcl  11983  lcmabs  11987  lcmgcdlem  11988  lcmdvds  11990  lcmgcdnn  11993  coprmdvds  12003  qredeq  12007  divgcdcoprm0  12012  divgcdcoprmex  12013  rpexp1i  12063  sqrt2irrlem  12070  sqpweven  12084  2sqpwodd  12085  sqrt2irraplemnn  12088  qmuldeneqnum  12104  nn0gcdsq  12109  numdensq  12111  nn0sqrtelqelz  12115  phibndlem  12125  dfphi2  12129  phiprmpw  12131  phiprm  12132  phimullem  12134  eulerthlem1  12136  eulerthlemh  12140  eulerthlemth  12141  eulerth  12142  prmdiv  12144  hashgcdlem  12147  phisum  12149  odzdvds  12154  vfermltl  12160  powm2modprm  12161  modprm0  12163  nnnn0modprm0  12164  coprimeprodsq  12166  pythagtriplem1  12174  pythagtriplem3  12176  pythagtriplem4  12177  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem14  12186  pythagtriplem16  12188  pceulem  12203  pcval  12205  pczpre  12206  pcdiv  12211  pc1  12214  pcrec  12217  pcexp  12218  pcid  12232  pcneg  12233  pcgcd1  12236  pc2dvds  12238  difsqpwdvds  12246  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmpt2  12251  pcprod  12253  pcfac  12257  ennnfonelemp1  12276  ennnfonelemhdmp1  12279  ennnfonelemss  12280  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemhom  12285  ennnfonelemnn0  12292  ctinfomlemom  12297  setsvala  12362  fvsetsid  12365  setsresg  12369  setscom  12371  setsslid  12381  ressid2  12390  ressval2  12391  restid2  12501  ntrval  12651  clsval  12652  cldcls  12655  neival  12684  resttop  12711  restco  12715  restabs  12716  resttopon2  12719  cnpval  12739  cnntr  12766  cnrest2  12777  upxp  12813  uptx  12815  cnmpt11  12824  cnmpt21  12832  psmetsym  12870  psmetres2  12874  xmetsym  12909  xmettxlem  13050  txmetcnp  13059  cnbl0  13075  cnblcld  13076  remetdval  13080  bl2ioo  13083  tgioo  13087  addcncntoplem  13092  divcnap  13096  fsumcncntop  13097  cncfmet  13120  cncfmptc  13123  addccncf  13127  negcncf  13129  mulcncflem  13131  ivthinclemlopn  13155  limcimolemlt  13174  cnplimcim  13177  cnplimclemr  13179  limccnp2lem  13186  limccnp2cntop  13187  dvfvalap  13191  dvconst  13202  dvaddxxbr  13206  dvmulxxbr  13207  dvcjbr  13213  dvexp  13216  dvrecap  13218  dvmptclx  13221  dvmptaddx  13222  dvmptmulx  13223  dvmptcmulcn  13224  dveflem  13228  dvef  13229  reeff1oleme  13234  sin0pilem1  13243  sin0pilem2  13244  efper  13269  sinperlem  13270  sinmpi  13277  cosmpi  13278  sinppi  13279  cosppi  13280  efimpi  13281  ptolemy  13286  sinq12gt0  13292  coseq0negpitopi  13298  tangtx  13300  abssinper  13308  cosq34lt1  13312  relogexp  13334  logdivlti  13343  logcxp  13359  rpcxp0  13360  rpcxp1  13361  1cxp  13362  ecxp  13363  rpcxpadd  13367  rpcxpp1  13368  rpmulcxp  13371  rpdivcxp  13373  cxpmul  13374  rpcxproot  13375  abscxp  13376  rpcxpsqrtth  13391  rplogbid1  13406  rplogb1  13407  rpelogb  13408  rplogbreexp  13412  rplogbzexp  13413  rprelogbmul  13414  rprelogbmulexp  13415  rprelogbdiv  13416  logbrec  13419  rpcxplogb  13423  logbgcd1irr  13426  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  binom4  13438  djucllem  13516  bj-charfun  13524  bj-charfundc  13525  bj-charfundcALT  13526  nninfsellemeq  13728  nninffeq  13734  qdencn  13740  cvgcmp2nlemabs  13745  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  apdifflemf  13759  redcwlpolemeq1  13767  dceqnconst  13772  dcapnconst  13773  nconstwlpolem0  13775  nconstwlpolemgt0  13776  nconstwlpolem  13777