Theorem eqtri 2228

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

Hypotheses

Ref	Expression
eqtri.1	|- A = B
eqtri.2	|- B = C

Assertion

Ref	Expression
eqtri	|- A = C

Proof of Theorem eqtri

Step	Hyp	Ref	Expression
1		eqtri.1	. 2 |- A = B
2		eqtri.2	. . 3 |- B = C
3	2	eqeq2i 2218	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 145	1 |- A = C

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200

This theorem is referenced by:  eqtr2i  2229  eqtr3i  2230  eqtr4i  2231  3eqtri  2232  3eqtrri  2233  3eqtr2i  2234  cbvrab  2774  csb2  3103  cbvrabcsf  3167  difjust  3175  unjust  3177  injust  3179  dfdif3  3291  difeq12i  3297  inrot  3396  symdif1  3446  rabnc  3501  0in  3504  ssdifin0  3550  dfif3  3593  ifbieq2i  3603  ifbieq12i  3605  pwjust  3627  snjust  3648  dfpr2  3662  disjpr2  3707  difprsn1  3783  diftpsn3  3785  difpr  3786  dfuni2  3866  intab  3928  intunsn  3937  rint0  3938  iunid  3997  viin  4001  iinrabm  4004  2iunin  4008  riin0  4013  iunxprg  4022  unopab  4139  cbvmptf  4154  cbvmpt  4155  exmid1stab  4268  unisucg  4479  op1stb  4543  orddif  4613  elxpi  4709  csbxpg  4774  relopabi  4821  inxp  4830  coeq12i  4859  dfdm3  4883  dfrn3  4885  dmun  4904  dmopab  4908  dmopab3  4910  dmxpid  4918  dmxpin  4919  rnopab  4944  rnmpt  4945  rncoss  4968  rncoeq  4971  reseq12i  4976  resundi  4991  resindi  4993  resiun1  4997  resdmdfsn  5021  resopab  5022  opabresid  5031  dfima3  5044  mptima  5053  imadisj  5063  ndmima  5078  mptcnv  5104  rnun  5110  rnuni  5113  imaundi  5114  inimass  5118  cnvxp  5120  rnxpm  5131  dminxp  5146  imainrect  5147  cnvcnv3  5151  dmpropg  5174  op1sta  5183  op2ndb  5185  op2nda  5186  resdmres  5193  mptpreima  5195  coundi  5203  coundir  5204  cocnvcnv1  5212  cores2  5214  dfdm2  5236  iotajust  5250  dfiota2  5252  funi  5322  funtp  5346  fntpg  5349  funcnvuni  5362  funcnvres  5366  imadiflem  5372  imadif  5373  imainlem  5374  imain  5375  fnresdisj  5405  mptfng  5421  resdif  5566  fv2  5594  dffv4g  5596  fveq12i  5605  nfvres  5633  0fv  5635  dfimafn2  5651  fnimapr  5662  fvmptss2  5677  fvmptg  5678  fvmpts  5680  fvmpt2  5686  mptfvex  5688  elfvmptrab  5698  fvopab6  5699  f1ompt  5754  dfmpt  5780  ressnop0  5788  fprg  5790  fvsnun1  5804  fsnunfv  5808  fvpr2g  5814  imauni  5853  fliftfuns  5890  cbvriota  5933  oveq123i  5981  fconstmpo  6063  resoprab  6064  mpofun  6070  rnmpo  6079  reldmmpo  6080  ov  6088  ovigg  6089  ovmpt4g  6091  ovg  6108  caov31  6159  elmpocl  6164  f1ocnvd  6171  oprabrexex2  6238  op1st  6255  op2nd  6256  f1stres  6268  f2ndres  6269  unielxp  6283  dfoprab3s  6299  dfoprab4  6301  mpompts  6307  mpofvex  6314  oprab2co  6327  df1st2  6328  df2nd2  6329  f1od2  6344  brtpos0  6361  tposoprab  6389  smores3  6402  tfrlemi14d  6442  tfr1onlemaccex  6457  tfrcllemaccex  6470  rdgisuc1  6493  rdg0  6496  frec0g  6506  df1o2  6538  df2o2  6540  oasuc  6573  omv2  6574  omsuc  6581  ecidsn  6692  qliftfuns  6729  oviec  6751  mapsncnv  6805  dfixp  6810  xpcomco  6946  xpassen  6950  ssenen  6973  undifdc  7047  unfiin  7049  fidcenumlemrks  7081  fidcenumlemr  7083  sbthlemi5  7089  sbthlemi8  7092  fi0  7103  inf00  7159  djuf1olemr  7182  djuinr  7191  djuin  7192  djuun  7195  casefun  7213  casedm  7214  caseinj  7217  caseinl  7219  caseinr  7220  endjusym  7224  eninl  7225  eninr  7226  djudm  7233  djuinj  7234  fodjuomni  7277  fodjumkv  7288  nninfwlporlemd  7300  pm54.43  7324  exmidfodomrlemim  7340  xp2dju  7358  djucomen  7359  djuassen  7360  xpdjuen  7361  pw1nel3  7377  sucpw1nel3  7379  addpiord  7464  mulpiord  7465  dmaddpi  7473  dmmulpi  7474  recmulnqg  7539  1lt2nq  7554  halfnqq  7558  dfmq0qs  7577  dfplq0qs  7578  genpdf  7656  1prl  7703  1pru  7704  ltexprlemell  7746  ltexprlemelu  7747  recexprlemell  7770  recexprlemelu  7771  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdrl  7805  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem2  7828  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem2  7858  addsrpr  7893  mulsrpr  7894  caucvgsrlemoffres  7948  caucvgsr  7950  suplocsrlempr  7955  addcnsr  7982  mulcnsr  7983  mulresr  7986  addvalex  7992  pitonnlem1  7993  axi2m1  8023  axcnre  8029  mulcomli  8114  mnfnre  8150  addcomli  8252  add42i  8273  mvrraddi  8324  neg0  8353  negdii  8391  negsubdi2i  8393  crap0  9066  2t2e4  9226  3t2e6  9228  3t3e9  9229  4t2e8  9230  neg1mulneg1e1  9284  8th4div3  9291  halfpm6th  9292  iap0  9295  dfdec10  9542  deceq12i  9547  numltc  9564  decsuc  9569  decsucc  9579  nummac  9583  numma2c  9584  numadd  9585  numaddc  9586  nummul1c  9587  nummul2c  9588  decma  9589  decmac  9590  decma2c  9591  decadd  9592  decaddc  9593  decrmanc  9595  decrmac  9596  decaddci  9599  decsubi  9601  decmul1  9602  decmul1c  9603  decmul2c  9604  11multnc  9606  4t3lem  9635  6t2e12  9642  7t2e14  9647  8t2e16  9653  9t2e18  9660  9t11e99  9668  halfthird  9681  5recm6rec  9682  divfnzn  9777  xnegpnf  9985  xneg0  9988  xaddmnf1  10005  xaddmnf2  10006  mnfaddpnf  10008  iooval2  10072  dfioo2  10131  fzval2  10168  fzsuc2  10236  fztpval  10240  fz0to3un2pr  10280  fz0to4untppr  10281  fzo01  10382  fzo12sn  10383  fzo0to42pr  10386  fldiv4p1lem1div2  10485  intqfrac2  10501  intfracq  10502  xnn0nnen  10619  1tonninf  10623  neg1sqe1  10816  sq2  10817  sq3  10818  cu2  10820  i2  10822  i3  10823  binom2i  10830  sq10  10894  3dec  10896  facp1  10912  fac2  10913  fac4  10915  4bc2eq6  10956  hashp1i  10992  pr0hash2ex  10997  hashfzo  11004  hashxp  11008  zfz1isolem1  11022  elovmpowrd  11072  ccat1st1st  11131  cji  11328  cnrecnv  11336  sqrt0  11430  resqrexlemover  11436  resqrexlemcalc3  11442  absi  11485  absimle  11510  sumeq12i  11791  summodclem2a  11807  summodc  11809  sum0  11814  fsumsplitf  11834  fsum2dlemstep  11860  fsumabs  11891  fsumiun  11903  0.999...  11947  mertenslem2  11962  prodeq12i  11989  prodmodc  12004  fprod2dlemstep  12048  ege2le3  12097  eft0val  12119  cos0  12156  cos1bnd  12185  cos2bnd  12186  3dvdsdec  12291  3dvds2dec  12292  odd2np1  12299  opoe  12321  nn0o  12333  5ndvds3  12360  5ndvds6  12361  bitsfzolem  12380  m1bits  12386  gcd0val  12396  6gcd4e2  12431  nnmindc  12470  nnminle  12471  3lcm2e6woprm  12523  3lcm2e6  12597  nn0gcdsq  12637  phiprmpw  12659  phimullem  12662  pcprecl  12727  pcprendvds  12728  pcmptdvds  12783  pockthi  12796  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  4sqlem19  12847  dec5nprm  12852  dec2nprm  12853  modxai  12854  modsubi  12857  numexp2x  12863  decsplit0b  12864  decsplit0  12865  decsplit  12867  karatsuba  12868  2exp5  12870  2exp7  12872  2exp8  12873  2exp11  12874  2exp16  12875  3exp3  12876  unennn  12883  ennnfonelemj0  12887  ennnfonelem0  12891  ennnfonelem1  12893  ennnfonelemhf1o  12899  ennnfonelemrn  12905  ennnfonelemdm  12906  strnfvnd  12967  slotslfn  12973  setsfun  12982  setsfun0  12983  setscom  12987  setsslid  12998  2strstr1g  13069  eqglact  13676  ecqusaddd  13689  ghmeqker  13722  dfrhm2  14031  rmodislmod  14228  cnfldadd  14439  cnfldmul  14441  expghmap  14484  fczpsrbag  14548  cnco  14808  txuni2  14843  txbas  14845  uptx  14861  txcn  14862  cnmptid  14868  cnmpt2t  14880  xmetxp  15094  cnmetdval  15116  remetdval  15134  resubmet  15143  rerestcntop  15145  rerest  15147  divcnap  15152  cnrehmeocntop  15197  dvexp  15298  plyun0  15323  plyco  15346  plycj  15348  sinhalfpilem  15378  cosneghalfpi  15385  efhalfpi  15386  cospi  15387  efipi  15388  eulerid  15389  sin2pi  15390  cos2pi  15391  ef2pi  15392  sincosq4sgn  15416  cosq14gt0  15419  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  sinkpi  15434  cosq34lt1  15437  dfrelog  15447  2logb9irr  15558  2logb9irrALT  15561  2logb9irrap  15564  mersenne  15584  perfectlem2  15587  zabsle1  15591  lgslem2  15593  lgsfcl2  15598  lgsdir2lem1  15620  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdir2lem5  15624  lgseisen  15666  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgs2  15694  2lgsoddprmlem3a  15699  2lgsoddprmlem3b  15700  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  pw0ss  15794  umgrislfupgrenlem  15836  ex-fl  15861  ex-exp  15863  ex-fac  15864  ex-bc  15865  ex-dvds  15866  ex-gcd  15867  bj-dfom  16068  012of  16130  2o01f  16131  pwle2  16137  nninfsellemqall  16154  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193  dceqnconst  16201  dcapnconst  16202  taupi  16214