Theorem eqtri 2217

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 2207	. 2 |- ( A = B <-> A = C )
4	1, 3	mpbi 145	1 |- A = C

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2i  2218  eqtr3i  2219  eqtr4i  2220  3eqtri  2221  3eqtrri  2222  3eqtr2i  2223  cbvrab  2761  csb2  3086  cbvrabcsf  3150  difjust  3158  unjust  3160  injust  3162  dfdif3  3273  difeq12i  3279  inrot  3378  symdif1  3428  rabnc  3483  0in  3486  ssdifin0  3532  dfif3  3574  ifbieq2i  3584  ifbieq12i  3586  pwjust  3606  snjust  3627  dfpr2  3641  disjpr2  3686  difprsn1  3761  diftpsn3  3763  difpr  3764  dfuni2  3841  intab  3903  intunsn  3912  rint0  3913  iunid  3972  viin  3976  iinrabm  3979  2iunin  3983  riin0  3988  iunxprg  3997  unopab  4112  cbvmptf  4127  cbvmpt  4128  exmid1stab  4241  unisucg  4449  op1stb  4513  orddif  4583  elxpi  4679  csbxpg  4744  relopabi  4791  inxp  4800  coeq12i  4829  dfdm3  4853  dfrn3  4855  dmun  4873  dmopab  4877  dmopab3  4879  dmxpid  4887  dmxpin  4888  rnopab  4913  rnmpt  4914  rncoss  4936  rncoeq  4939  reseq12i  4944  resundi  4959  resindi  4961  resiun1  4965  resdmdfsn  4989  resopab  4990  opabresid  4999  dfima3  5012  mptima  5021  imadisj  5031  ndmima  5046  mptcnv  5072  rnun  5078  rnuni  5081  imaundi  5082  inimass  5086  cnvxp  5088  rnxpm  5099  dminxp  5114  imainrect  5115  cnvcnv3  5119  dmpropg  5142  op1sta  5151  op2ndb  5153  op2nda  5154  resdmres  5161  mptpreima  5163  coundi  5171  coundir  5172  cocnvcnv1  5180  cores2  5182  dfdm2  5204  iotajust  5218  dfiota2  5220  funi  5290  funtp  5311  fntpg  5314  funcnvuni  5327  funcnvres  5331  imadiflem  5337  imadif  5338  imainlem  5339  imain  5340  fnresdisj  5368  mptfng  5383  resdif  5526  fv2  5553  dffv4g  5555  fveq12i  5564  nfvres  5592  0fv  5594  dfimafn2  5610  fnimapr  5621  fvmptss2  5636  fvmptg  5637  fvmpts  5639  fvmpt2  5645  mptfvex  5647  elfvmptrab  5657  fvopab6  5658  f1ompt  5713  dfmpt  5739  ressnop0  5743  fprg  5745  fvsnun1  5759  fsnunfv  5763  fvpr2g  5769  imauni  5808  fliftfuns  5845  cbvriota  5888  oveq123i  5936  fconstmpo  6017  resoprab  6018  mpofun  6024  rnmpo  6033  reldmmpo  6034  ov  6042  ovigg  6043  ovmpt4g  6045  ovg  6062  caov31  6113  elmpocl  6118  f1ocnvd  6125  oprabrexex2  6187  op1st  6204  op2nd  6205  f1stres  6217  f2ndres  6218  unielxp  6232  dfoprab3s  6248  dfoprab4  6250  mpompts  6256  mpofvex  6263  oprab2co  6276  df1st2  6277  df2nd2  6278  f1od2  6293  brtpos0  6310  tposoprab  6338  smores3  6351  tfrlemi14d  6391  tfr1onlemaccex  6406  tfrcllemaccex  6419  rdgisuc1  6442  rdg0  6445  frec0g  6455  df1o2  6487  df2o2  6489  oasuc  6522  omv2  6523  omsuc  6530  ecidsn  6641  qliftfuns  6678  oviec  6700  mapsncnv  6754  dfixp  6759  xpcomco  6885  xpassen  6889  ssenen  6912  undifdc  6985  unfiin  6987  fidcenumlemrks  7019  fidcenumlemr  7021  sbthlemi5  7027  sbthlemi8  7030  fi0  7041  inf00  7097  djuf1olemr  7120  djuinr  7129  djuin  7130  djuun  7133  casefun  7151  casedm  7152  caseinj  7155  caseinl  7157  caseinr  7158  endjusym  7162  eninl  7163  eninr  7164  djudm  7171  djuinj  7172  fodjuomni  7215  fodjumkv  7226  nninfwlporlemd  7238  pm54.43  7257  exmidfodomrlemim  7268  xp2dju  7282  djucomen  7283  djuassen  7284  xpdjuen  7285  pw1nel3  7298  sucpw1nel3  7300  addpiord  7383  mulpiord  7384  dmaddpi  7392  dmmulpi  7393  recmulnqg  7458  1lt2nq  7473  halfnqq  7477  dfmq0qs  7496  dfplq0qs  7497  genpdf  7575  1prl  7622  1pru  7623  ltexprlemell  7665  ltexprlemelu  7666  recexprlemell  7689  recexprlemelu  7690  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdrl  7724  cauappcvgprlem2  7727  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem2  7747  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem2  7777  addsrpr  7812  mulsrpr  7813  caucvgsrlemoffres  7867  caucvgsr  7869  suplocsrlempr  7874  addcnsr  7901  mulcnsr  7902  mulresr  7905  addvalex  7911  pitonnlem1  7912  axi2m1  7942  axcnre  7948  mulcomli  8033  mnfnre  8069  addcomli  8171  add42i  8192  mvrraddi  8243  neg0  8272  negdii  8310  negsubdi2i  8312  crap0  8985  2t2e4  9145  3t2e6  9147  3t3e9  9148  4t2e8  9149  neg1mulneg1e1  9203  8th4div3  9210  halfpm6th  9211  iap0  9214  dfdec10  9460  deceq12i  9465  numltc  9482  decsuc  9487  decsucc  9497  nummac  9501  numma2c  9502  numadd  9503  numaddc  9504  nummul1c  9505  nummul2c  9506  decma  9507  decmac  9508  decma2c  9509  decadd  9510  decaddc  9511  decrmanc  9513  decrmac  9514  decaddci  9517  decsubi  9519  decmul1  9520  decmul1c  9521  decmul2c  9522  11multnc  9524  4t3lem  9553  6t2e12  9560  7t2e14  9565  8t2e16  9571  9t2e18  9578  9t11e99  9586  halfthird  9599  5recm6rec  9600  divfnzn  9695  xnegpnf  9903  xneg0  9906  xaddmnf1  9923  xaddmnf2  9924  mnfaddpnf  9926  iooval2  9990  dfioo2  10049  fzval2  10086  fzsuc2  10154  fztpval  10158  fz0to3un2pr  10198  fz0to4untppr  10199  fzo01  10292  fzo12sn  10293  fzo0to42pr  10296  fldiv4p1lem1div2  10395  intqfrac2  10411  intfracq  10412  xnn0nnen  10529  1tonninf  10533  neg1sqe1  10726  sq2  10727  sq3  10728  cu2  10730  i2  10732  i3  10733  binom2i  10740  sq10  10804  3dec  10806  facp1  10822  fac2  10823  fac4  10825  4bc2eq6  10866  hashp1i  10902  pr0hash2ex  10907  hashfzo  10914  hashxp  10918  zfz1isolem1  10932  elovmpowrd  10976  cji  11067  cnrecnv  11075  sqrt0  11169  resqrexlemover  11175  resqrexlemcalc3  11181  absi  11224  absimle  11249  sumeq12i  11530  summodclem2a  11546  summodc  11548  sum0  11553  fsumsplitf  11573  fsum2dlemstep  11599  fsumabs  11630  fsumiun  11642  0.999...  11686  mertenslem2  11701  prodeq12i  11728  prodmodc  11743  fprod2dlemstep  11787  ege2le3  11836  eft0val  11858  cos0  11895  cos1bnd  11924  cos2bnd  11925  3dvdsdec  12030  3dvds2dec  12031  odd2np1  12038  opoe  12060  nn0o  12072  5ndvds3  12099  5ndvds6  12100  bitsfzolem  12118  gcd0val  12127  6gcd4e2  12162  nnmindc  12201  nnminle  12202  3lcm2e6woprm  12254  3lcm2e6  12328  nn0gcdsq  12368  phiprmpw  12390  phimullem  12393  pcprecl  12458  pcprendvds  12459  pcmptdvds  12514  pockthi  12527  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  4sqlem19  12578  dec5nprm  12583  dec2nprm  12584  modxai  12585  modsubi  12588  numexp2x  12594  decsplit0b  12595  decsplit0  12596  decsplit  12598  karatsuba  12599  2exp5  12601  2exp7  12603  2exp8  12604  2exp11  12605  2exp16  12606  3exp3  12607  unennn  12614  ennnfonelemj0  12618  ennnfonelem0  12622  ennnfonelem1  12624  ennnfonelemhf1o  12630  ennnfonelemrn  12636  ennnfonelemdm  12637  strnfvnd  12698  slotslfn  12704  setsfun  12713  setsfun0  12714  setscom  12718  setsslid  12729  2strstr1g  12799  eqglact  13355  ecqusaddd  13368  ghmeqker  13401  dfrhm2  13710  rmodislmod  13907  cnfldadd  14118  cnfldmul  14120  expghmap  14163  fczpsrbag  14225  cnco  14457  txuni2  14492  txbas  14494  uptx  14510  txcn  14511  cnmptid  14517  cnmpt2t  14529  xmetxp  14743  cnmetdval  14765  remetdval  14783  resubmet  14792  rerestcntop  14794  rerest  14796  divcnap  14801  cnrehmeocntop  14846  dvexp  14947  plyun0  14972  plyco  14995  plycj  14997  sinhalfpilem  15027  cosneghalfpi  15034  efhalfpi  15035  cospi  15036  efipi  15037  eulerid  15038  sin2pi  15039  cos2pi  15040  ef2pi  15041  sincosq4sgn  15065  cosq14gt0  15068  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  sinkpi  15083  cosq34lt1  15086  dfrelog  15096  2logb9irr  15207  2logb9irrALT  15210  2logb9irrap  15213  mersenne  15233  perfectlem2  15236  zabsle1  15240  lgslem2  15242  lgsfcl2  15247  lgsdir2lem1  15269  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdir2lem5  15273  lgseisen  15315  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgs2  15343  2lgsoddprmlem3a  15348  2lgsoddprmlem3b  15349  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  ex-fl  15371  ex-exp  15373  ex-fac  15374  ex-bc  15375  ex-dvds  15376  ex-gcd  15377  bj-dfom  15579  012of  15640  2o01f  15641  pwle2  15643  nninfsellemqall  15659  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696  dceqnconst  15704  dcapnconst  15705  taupi  15717