Theorem eqtrd 2172

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 2151	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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 2121

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

This theorem is referenced by:  eqtr2d  2173  eqtr3d  2174  eqtr4d  2175  3eqtrd  2176  3eqtrrd  2177  3eqtr2d  2178  syl5eq  2184  syl6eq  2188  rabeqbidv  2681  rabeqbidva  2682  csbidmg  3056  csbco3g  3058  difeq12d  3195  ifeq12d  3491  ifbieq1d  3494  ifbieq2d  3496  ifbieq12d  3498  eqifdc  3506  csbsng  3584  disjpr2  3587  csbunig  3744  iuneq12d  3837  unisn3  4366  op1stbg  4400  opthreg  4471  onsucuni2  4479  csbxpg  4620  coeq12d  4703  csbdmg  4733  reseq12d  4820  csbresg  4822  resima2  4853  imaeq12d  4882  csbrng  5000  opswapg  5025  relcnvtr  5058  relcoi2  5069  relcoi1  5070  iotaint  5101  funprg  5173  funtpg  5174  funcnvres2  5198  fnco  5231  fococnv2  5393  fveq12d  5428  csbfv12g  5457  csbfv2g  5458  csbfvg  5459  dffn5im  5467  funfvdm2  5485  fvun1  5487  fvmpt2d  5507  fvmptt  5512  fndmin  5527  fniniseg2  5542  fnniniseg2  5543  fmptcof  5587  fvresi  5613  fvunsng  5614  fvpr1g  5626  fvpr2g  5627  fvtp1g  5628  funiunfvdm  5664  fcof1o  5690  riotaeqbidv  5733  oveq123d  5795  csbov12g  5810  csbov1g  5811  csbov2g  5812  ovmpodxf  5896  caov42d  5957  caovdilemd  5962  caovimo  5964  grprinvd  5966  offeq  5995  offval2  5997  caofinvl  6004  ot1stg  6050  ot2ndg  6051  2nd1st  6078  mpomptsx  6095  dmmpossx  6097  fmpox  6098  fmpoco  6113  1stconst  6118  algrflemg  6127  tfrexlem  6231  rdgivallem  6278  rdgisuc1  6281  frec0g  6294  frecabcl  6296  frecsuclem  6303  frecrdg  6305  oa0  6353  oasuc  6360  oa1suc  6363  omsuc  6368  nnaass  6381  nndi  6382  nnmass  6383  nnm2  6421  nn2m  6422  ereq1  6436  errn  6451  uniqs2  6489  oviec  6535  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  mapsnconst  6588  mapen  6740  mapxpen  6742  xpmapenlem  6743  phplem4on  6761  fidifsnen  6764  undifdc  6812  fiintim  6817  fisseneq  6820  snexxph  6838  sbthlemi4  6848  sbthlemi6  6850  supeq2  6876  eqsupti  6883  infvalti  6909  djuf1olem  6938  djuss  6955  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  updjudhcoinlf  6965  updjudhcoinrg  6966  omp1eomlem  6979  difinfsn  6985  ctmlemr  6993  ctssdclemn0  6995  ctssdc  6998  enumctlemm  6999  en2other2  7052  mulidpi  7126  addasspig  7138  mulasspig  7140  distrpig  7141  indpi  7150  addcmpblnq  7175  mulpipq  7180  dmaddpqlem  7185  nqpi  7186  addcomnqg  7189  recrecnq  7202  ltsonq  7206  ltanqg  7208  ltmnqg  7209  ltaddnq  7215  ltexnqq  7216  archnqq  7225  prarloclemarch  7226  ltrnqg  7228  ltnnnq  7231  nq0nn  7250  addcmpblnq0  7251  nqpnq0nq  7261  nqnq0a  7262  nq0m0r  7264  nq0a0  7265  distrnq0  7267  addassnq0  7270  nq02m  7273  prarloclemlo  7302  prarloclemcalc  7310  addnqprllem  7335  addnqprulem  7336  addnqprl  7337  addnqpru  7338  appdivnq  7371  mulnqprl  7376  mulnqpru  7377  addcanprlemu  7423  ltaprlem  7426  ltmprr  7450  cauappcvgprlemladdrl  7465  mulcmpblnrlemg  7548  mulcomsrg  7565  distrsrg  7567  ltsosr  7572  1idsr  7576  00sr  7577  ltasrg  7578  recexgt0sr  7581  srpospr  7591  prsradd  7594  prsrriota  7596  caucvgsrlemcau  7601  caucvgsrlemgt1  7603  caucvgsrlemoffval  7604  caucvgsrlemoffres  7608  caucvgsr  7610  map2psrprg  7613  elreal2  7638  mulresr  7646  pitonnlem1p1  7654  pitonnlem2  7655  pitoregt0  7657  recidpirqlemcalc  7665  recidpirq  7666  axaddcl  7672  axmulcl  7674  axmulcom  7679  axmulass  7681  axdistr  7682  ax1rid  7685  axcnre  7689  recriota  7698  axcaucvglemcau  7706  mulid1  7763  mulid2  7764  adddirp1d  7792  joinlmuladdmuld  7793  muladd11  7895  1p1times  7896  readdcan  7902  comraddd  7919  add42  7924  npcan  7971  addsubass  7972  2addsub  7976  addsubeq4  7977  nppcan  7984  nnpcan  7985  npncan2  7989  nncan  7991  subsub  7992  nnncan  7997  nnncan1  7998  pnpcan2  8002  pnncan  8003  subneg  8011  negneg  8012  negdi2  8020  mvrraddd  8128  assraddsubd  8130  subaddeqd  8131  addid0  8135  mul02  8149  mul01  8151  mulneg1  8157  mul2neg  8160  mulm1  8162  ltadd2  8181  rimul  8347  rereim  8348  mulreim  8366  recextlem1  8412  mulcanapd  8422  divcanap1  8441  divrecap2  8449  divmulassap  8455  divmulasscomap  8456  divcanap4  8459  dividap  8461  muldivdirap  8467  divdivdivap  8473  recdivap  8478  divadddivap  8487  divsubdivap  8488  div2negap  8495  divcanap5rd  8578  dmdcanap2d  8581  subrecap  8598  recgt0  8608  lt2mul2div  8637  nnmulcl  8741  times2  8849  add1p1  8969  sub1m1  8970  cnm2m1cnm3  8971  nn0supp  9029  peano2z  9090  nneoor  9153  supminfex  9392  cnref1o  9440  rexneg  9613  xaddpnf1  9629  xaddmnf1  9631  rexadd  9635  xaddid1  9645  xaddid2  9646  xaddass  9652  xpncan  9654  xleadd1a  9656  xltadd1  9659  xposdif  9665  xadd4d  9668  xleaddadd  9670  iooidg  9692  iooval2  9698  icoshftf1o  9774  lincmb01cmp  9786  iccf1o  9787  fzval2  9793  fzsuc  9849  fzpred  9850  fztpval  9863  fseq1p1m1  9874  fzshftral  9888  fzo0to3tp  9996  fzo0sn0fzo1  9998  fzosplitsn  10010  fzosplitprm1  10011  fzisfzounsn  10013  rebtwn2zlemstep  10030  2tnp1ge0ge0  10074  flqdiv  10094  modqvalr  10098  modqdiffl  10108  modqfrac  10110  modqmulnn  10115  modqid  10122  modqcyc  10132  modqcyc2  10133  mulp1mod1  10138  modqmuladd  10139  modqmuladdnn0  10141  qnegmod  10142  m1modnnsub1  10143  addmodid  10145  addmodidr  10146  modqmul12d  10151  modqnegd  10152  modqadd12d  10153  modifeq2int  10159  modqaddmulmod  10164  modqdi  10165  modqsubdir  10166  modsumfzodifsn  10169  addmodlteq  10171  frec2uzsucd  10174  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdglem  10184  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdgdomlem  10190  frecuzrdgfunlem  10192  frecuzrdgtclt  10194  frecuzrdgsuctlem  10196  frecfzennn  10199  seqeq1  10221  seq3val  10231  seqvalcd  10232  seq3p1  10235  seqp1cd  10239  seq3feq2  10243  seq3fveq  10244  seq3shft2  10246  seq3-1p  10253  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemnanb  10263  iseqf1olemqk  10267  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1o  10277  seq3id3  10280  seq3z  10284  fser0const  10289  exp3vallem  10294  expnnval  10296  expp1  10300  expn1ap0  10303  mulexp  10332  expaddzaplem  10336  expaddzap  10337  expmul  10338  expp1zap  10342  expm1ap  10343  sqval  10351  iexpcyc  10397  subsq2  10400  binom2  10403  binom21  10404  binom2sub1  10406  mulbinom2  10408  binom3  10409  zesq  10410  bernneq  10412  sqoddm1div8  10444  nn0opthlem1d  10466  facp1  10476  faclbnd6  10490  bcval2  10496  bcval3  10497  bcn0  10501  bcp1n  10507  bcp1nk  10508  bcn2  10510  bcp1m1  10511  bcpasc  10512  bcn2m1  10515  hashinfom  10524  hashennn  10526  hashfz1  10529  fseq1hash  10547  omgadd  10548  hashunsng  10553  hashprg  10554  hashdifsn  10565  hashdifpr  10566  hashfz  10567  hashfzo  10568  hashfzo0  10569  hashfzp1  10570  hashfz0  10571  hashxp  10572  resunimafz0  10574  fnfz0hash  10575  ffzo0hash  10577  hashfacen  10579  zfz1isolemsplit  10581  zfz1isolemiso  10582  zfz1isolem1  10583  shftdm  10594  shftval2  10598  shftval4  10600  shftval5  10601  shftcan1  10606  seq3shft  10610  imre  10623  crre  10629  remim  10632  reim0b  10634  recj  10639  reneg  10640  readd  10641  resub  10642  remullem  10643  imcj  10647  imneg  10648  imadd  10649  imsub  10650  cjcj  10655  cjadd  10656  ipcnval  10658  cjneg  10662  cjsub  10664  cjexp  10665  imval2  10666  cjap  10678  resqrexlemf1  10780  resqrexlemfp1  10781  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemcvg  10791  resqrtcl  10801  sqrtsq  10816  absneg  10822  absvalsq  10825  absvalsq2  10826  sqabsadd  10827  sqabssub  10828  absval2  10829  absreimsq  10839  absmul  10841  absexp  10851  absexpzap  10852  abssuble0  10875  abstri  10876  recan  10881  amgm2  10890  maxabslemlub  10979  max0addsup  10991  minmax  11001  minabs  11007  bdtrilem  11010  bdtri  11011  xrmaxiflemab  11016  xrmaxiflemcom  11018  xrmaxadd  11030  xrminmax  11034  xrmineqinf  11038  xrminrecl  11042  xrbdtri  11045  climshft2  11075  subcn2  11080  reccn2ap  11082  climaddc2  11099  iser3shft  11115  climcvg1nlem  11118  sumeq12dv  11141  sumeq12rdv  11142  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  summodc  11152  fsum3  11156  isumz  11158  fsumf1o  11159  fisumss  11161  fsumsersdc  11164  fsum3ser  11166  fsumsplit  11176  fsumsplitf  11177  sumsnf  11178  fsumsplitsn  11179  fsum1  11181  sumpr  11182  sumtp  11183  fsumm1  11185  fsum1p  11187  fsumsplitsnun  11188  fsump1  11189  isumclim  11190  sumnul  11193  isumadd  11200  fsum2dlemstep  11203  fsumcnv  11206  fisumcom2  11207  fsumshftm  11214  fisumrev2  11215  fisum0diag2  11216  fsumsub  11221  fsumdifsnconst  11224  modfsummodlemstep  11226  fsumabs  11234  telfsumo  11235  telfsum  11237  telfsum2  11238  fsumparts  11239  fsumiun  11246  hashiun  11247  hash2iun  11248  hash2iun1dif1  11249  binomlem  11252  binom1p  11254  binom11  11255  binom1dif  11256  bcxmas  11258  isum1p  11261  isumnn0nn  11262  isumlessdc  11265  divcnv  11266  arisum2  11268  trireciplem  11269  geosergap  11275  geolim  11280  georeclim  11282  geo2lim  11285  geoisum1  11288  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemsumlt  11297  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodfrecap  11315  prodeq12dv  11338  prodeq12rdv  11339  prodrbdclem  11340  fproddccvg  11341  prodmodclem3  11344  prodmodclem2a  11345  eftabs  11362  efcllemp  11364  ef0lem  11366  efcvgfsum  11373  ege2le3  11377  efcj  11379  efaddlem  11380  efexp  11388  eftlub  11396  efsep  11397  effsumlt  11398  ef4p  11400  efgt1p2  11401  efgt1p  11402  tanval2ap  11420  tanval3ap  11421  resinval  11422  recosval  11423  efi4p  11424  resin4p  11425  recos4p  11426  sinneg  11433  cosneg  11434  tannegap  11435  efmival  11440  sinadd  11443  cosadd  11444  tanaddaplem  11445  tanaddap  11446  sinsub  11447  cossub  11448  addsin  11449  subsin  11450  subcos  11454  sincossq  11455  sin2t  11456  sin01bnd  11464  cos01bnd  11465  absefi  11475  absef  11476  absefib  11477  efieq1re  11478  demoivre  11479  demoivreALT  11480  eirraplem  11483  dvdstr  11530  dvdsadd2b  11540  mulmoddvds  11561  ltoddhalfle  11590  opoe  11592  m1expo  11597  m1exp1  11598  flodddiv4  11631  flodddiv4t2lthalf  11634  zsupcllemstep  11638  nn0gcdid0  11669  gcdaddm  11672  gcdadd  11673  gcdid  11674  gcdabs  11676  modgcd  11679  1gcd  11680  bezout  11699  dfgcd2  11702  mulgcd  11704  absmulgcd  11705  gcdmultiple  11708  gcdmultiplez  11709  rpmulgcd  11714  rplpwr  11715  rppwr  11716  dvdssqlem  11718  ialgr0  11725  alginv  11728  algcvg  11729  algfx  11733  eucalginv  11737  eucalglt  11738  lcmcl  11753  lcmabs  11757  lcmgcdlem  11758  lcmdvds  11760  lcmgcdnn  11763  coprmdvds  11773  qredeq  11777  divgcdcoprm0  11782  divgcdcoprmex  11783  rpexp1i  11832  sqrt2irrlem  11839  sqpweven  11853  2sqpwodd  11854  sqrt2irraplemnn  11857  qmuldeneqnum  11873  nn0gcdsq  11878  numdensq  11880  nn0sqrtelqelz  11884  phibndlem  11892  dfphi2  11896  phiprmpw  11898  phiprm  11899  phimullem  11901  hashgcdlem  11903  ennnfonelemp1  11919  ennnfonelemhdmp1  11922  ennnfonelemss  11923  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  ennnfonelemnn0  11935  ctinfomlemom  11940  setsvala  11990  fvsetsid  11993  setsresg  11997  setscom  11999  setsslid  12009  ressid2  12018  ressval2  12019  restid2  12129  ntrval  12279  clsval  12280  cldcls  12283  neival  12312  resttop  12339  restco  12343  restabs  12344  resttopon2  12347  cnpval  12367  cnntr  12394  cnrest2  12405  upxp  12441  uptx  12443  cnmpt11  12452  cnmpt21  12460  psmetsym  12498  psmetres2  12502  xmetsym  12537  xmettxlem  12678  txmetcnp  12687  cnbl0  12703  cnblcld  12704  remetdval  12708  bl2ioo  12711  tgioo  12715  addcncntoplem  12720  divcnap  12724  fsumcncntop  12725  cncfmet  12748  cncfmptc  12751  addccncf  12755  negcncf  12757  mulcncflem  12759  ivthinclemlopn  12783  limcimolemlt  12802  cnplimcim  12805  cnplimclemr  12807  limccnp2lem  12814  limccnp2cntop  12815  dvfvalap  12819  dvconst  12830  dvaddxxbr  12834  dvmulxxbr  12835  dvcjbr  12841  dvexp  12844  dvrecap  12846  dvmptclx  12849  dvmptaddx  12850  dvmptmulx  12851  dvmptcmulcn  12852  dveflem  12855  dvef  12856  sin0pilem1  12862  sin0pilem2  12863  efper  12888  sinperlem  12889  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899  efimpi  12900  ptolemy  12905  sinq12gt0  12911  coseq0negpitopi  12917  tangtx  12919  abssinper  12927  cosq34lt1  12931  djucllem  13007  nninfalllemn  13202  nninfsellemeq  13210  nninffeq  13216  qdencn  13222  cvgcmp2nlemabs  13227  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234