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  3274  difeq12i  3280  inrot  3379  symdif1  3429  rabnc  3484  0in  3487  ssdifin0  3533  dfif3  3575  ifbieq2i  3585  ifbieq12i  3587  pwjust  3607  snjust  3628  dfpr2  3642  disjpr2  3687  difprsn1  3762  diftpsn3  3764  difpr  3765  dfuni2  3842  intab  3904  intunsn  3913  rint0  3914  iunid  3973  viin  3977  iinrabm  3980  2iunin  3984  riin0  3989  iunxprg  3998  unopab  4113  cbvmptf  4128  cbvmpt  4129  exmid1stab  4242  unisucg  4450  op1stb  4514  orddif  4584  elxpi  4680  csbxpg  4745  relopabi  4792  inxp  4801  coeq12i  4830  dfdm3  4854  dfrn3  4856  dmun  4874  dmopab  4878  dmopab3  4880  dmxpid  4888  dmxpin  4889  rnopab  4914  rnmpt  4915  rncoss  4937  rncoeq  4940  reseq12i  4945  resundi  4960  resindi  4962  resiun1  4966  resdmdfsn  4990  resopab  4991  opabresid  5000  dfima3  5013  mptima  5022  imadisj  5032  ndmima  5047  mptcnv  5073  rnun  5079  rnuni  5082  imaundi  5083  inimass  5087  cnvxp  5089  rnxpm  5100  dminxp  5115  imainrect  5116  cnvcnv3  5120  dmpropg  5143  op1sta  5152  op2ndb  5154  op2nda  5155  resdmres  5162  mptpreima  5164  coundi  5172  coundir  5173  cocnvcnv1  5181  cores2  5183  dfdm2  5205  iotajust  5219  dfiota2  5221  funi  5291  funtp  5312  fntpg  5315  funcnvuni  5328  funcnvres  5332  imadiflem  5338  imadif  5339  imainlem  5340  imain  5341  fnresdisj  5371  mptfng  5386  resdif  5529  fv2  5556  dffv4g  5558  fveq12i  5567  nfvres  5595  0fv  5597  dfimafn2  5613  fnimapr  5624  fvmptss2  5639  fvmptg  5640  fvmpts  5642  fvmpt2  5648  mptfvex  5650  elfvmptrab  5660  fvopab6  5661  f1ompt  5716  dfmpt  5742  ressnop0  5746  fprg  5748  fvsnun1  5762  fsnunfv  5766  fvpr2g  5772  imauni  5811  fliftfuns  5848  cbvriota  5891  oveq123i  5939  fconstmpo  6021  resoprab  6022  mpofun  6028  rnmpo  6037  reldmmpo  6038  ov  6046  ovigg  6047  ovmpt4g  6049  ovg  6066  caov31  6117  elmpocl  6122  f1ocnvd  6129  oprabrexex2  6196  op1st  6213  op2nd  6214  f1stres  6226  f2ndres  6227  unielxp  6241  dfoprab3s  6257  dfoprab4  6259  mpompts  6265  mpofvex  6272  oprab2co  6285  df1st2  6286  df2nd2  6287  f1od2  6302  brtpos0  6319  tposoprab  6347  smores3  6360  tfrlemi14d  6400  tfr1onlemaccex  6415  tfrcllemaccex  6428  rdgisuc1  6451  rdg0  6454  frec0g  6464  df1o2  6496  df2o2  6498  oasuc  6531  omv2  6532  omsuc  6539  ecidsn  6650  qliftfuns  6687  oviec  6709  mapsncnv  6763  dfixp  6768  xpcomco  6894  xpassen  6898  ssenen  6921  undifdc  6994  unfiin  6996  fidcenumlemrks  7028  fidcenumlemr  7030  sbthlemi5  7036  sbthlemi8  7039  fi0  7050  inf00  7106  djuf1olemr  7129  djuinr  7138  djuin  7139  djuun  7142  casefun  7160  casedm  7161  caseinj  7164  caseinl  7166  caseinr  7167  endjusym  7171  eninl  7172  eninr  7173  djudm  7180  djuinj  7181  fodjuomni  7224  fodjumkv  7235  nninfwlporlemd  7247  pm54.43  7269  exmidfodomrlemim  7280  xp2dju  7298  djucomen  7299  djuassen  7300  xpdjuen  7301  pw1nel3  7314  sucpw1nel3  7316  addpiord  7400  mulpiord  7401  dmaddpi  7409  dmmulpi  7410  recmulnqg  7475  1lt2nq  7490  halfnqq  7494  dfmq0qs  7513  dfplq0qs  7514  genpdf  7592  1prl  7639  1pru  7640  ltexprlemell  7682  ltexprlemelu  7683  recexprlemell  7706  recexprlemelu  7707  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdrl  7741  cauappcvgprlem2  7744  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem2  7764  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem2  7794  addsrpr  7829  mulsrpr  7830  caucvgsrlemoffres  7884  caucvgsr  7886  suplocsrlempr  7891  addcnsr  7918  mulcnsr  7919  mulresr  7922  addvalex  7928  pitonnlem1  7929  axi2m1  7959  axcnre  7965  mulcomli  8050  mnfnre  8086  addcomli  8188  add42i  8209  mvrraddi  8260  neg0  8289  negdii  8327  negsubdi2i  8329  crap0  9002  2t2e4  9162  3t2e6  9164  3t3e9  9165  4t2e8  9166  neg1mulneg1e1  9220  8th4div3  9227  halfpm6th  9228  iap0  9231  dfdec10  9477  deceq12i  9482  numltc  9499  decsuc  9504  decsucc  9514  nummac  9518  numma2c  9519  numadd  9520  numaddc  9521  nummul1c  9522  nummul2c  9523  decma  9524  decmac  9525  decma2c  9526  decadd  9527  decaddc  9528  decrmanc  9530  decrmac  9531  decaddci  9534  decsubi  9536  decmul1  9537  decmul1c  9538  decmul2c  9539  11multnc  9541  4t3lem  9570  6t2e12  9577  7t2e14  9582  8t2e16  9588  9t2e18  9595  9t11e99  9603  halfthird  9616  5recm6rec  9617  divfnzn  9712  xnegpnf  9920  xneg0  9923  xaddmnf1  9940  xaddmnf2  9941  mnfaddpnf  9943  iooval2  10007  dfioo2  10066  fzval2  10103  fzsuc2  10171  fztpval  10175  fz0to3un2pr  10215  fz0to4untppr  10216  fzo01  10309  fzo12sn  10310  fzo0to42pr  10313  fldiv4p1lem1div2  10412  intqfrac2  10428  intfracq  10429  xnn0nnen  10546  1tonninf  10550  neg1sqe1  10743  sq2  10744  sq3  10745  cu2  10747  i2  10749  i3  10750  binom2i  10757  sq10  10821  3dec  10823  facp1  10839  fac2  10840  fac4  10842  4bc2eq6  10883  hashp1i  10919  pr0hash2ex  10924  hashfzo  10931  hashxp  10935  zfz1isolem1  10949  elovmpowrd  10993  cji  11084  cnrecnv  11092  sqrt0  11186  resqrexlemover  11192  resqrexlemcalc3  11198  absi  11241  absimle  11266  sumeq12i  11547  summodclem2a  11563  summodc  11565  sum0  11570  fsumsplitf  11590  fsum2dlemstep  11616  fsumabs  11647  fsumiun  11659  0.999...  11703  mertenslem2  11718  prodeq12i  11745  prodmodc  11760  fprod2dlemstep  11804  ege2le3  11853  eft0val  11875  cos0  11912  cos1bnd  11941  cos2bnd  11942  3dvdsdec  12047  3dvds2dec  12048  odd2np1  12055  opoe  12077  nn0o  12089  5ndvds3  12116  5ndvds6  12117  bitsfzolem  12136  m1bits  12142  gcd0val  12152  6gcd4e2  12187  nnmindc  12226  nnminle  12227  3lcm2e6woprm  12279  3lcm2e6  12353  nn0gcdsq  12393  phiprmpw  12415  phimullem  12418  pcprecl  12483  pcprendvds  12484  pcmptdvds  12539  pockthi  12552  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  4sqlem19  12603  dec5nprm  12608  dec2nprm  12609  modxai  12610  modsubi  12613  numexp2x  12619  decsplit0b  12620  decsplit0  12621  decsplit  12623  karatsuba  12624  2exp5  12626  2exp7  12628  2exp8  12629  2exp11  12630  2exp16  12631  3exp3  12632  unennn  12639  ennnfonelemj0  12643  ennnfonelem0  12647  ennnfonelem1  12649  ennnfonelemhf1o  12655  ennnfonelemrn  12661  ennnfonelemdm  12662  strnfvnd  12723  slotslfn  12729  setsfun  12738  setsfun0  12739  setscom  12743  setsslid  12754  2strstr1g  12824  eqglact  13431  ecqusaddd  13444  ghmeqker  13477  dfrhm2  13786  rmodislmod  13983  cnfldadd  14194  cnfldmul  14196  expghmap  14239  fczpsrbag  14301  cnco  14541  txuni2  14576  txbas  14578  uptx  14594  txcn  14595  cnmptid  14601  cnmpt2t  14613  xmetxp  14827  cnmetdval  14849  remetdval  14867  resubmet  14876  rerestcntop  14878  rerest  14880  divcnap  14885  cnrehmeocntop  14930  dvexp  15031  plyun0  15056  plyco  15079  plycj  15081  sinhalfpilem  15111  cosneghalfpi  15118  efhalfpi  15119  cospi  15120  efipi  15121  eulerid  15122  sin2pi  15123  cos2pi  15124  ef2pi  15125  sincosq4sgn  15149  cosq14gt0  15152  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  sinkpi  15167  cosq34lt1  15170  dfrelog  15180  2logb9irr  15291  2logb9irrALT  15294  2logb9irrap  15297  mersenne  15317  perfectlem2  15320  zabsle1  15324  lgslem2  15326  lgsfcl2  15331  lgsdir2lem1  15353  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdir2lem5  15357  lgseisen  15399  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgs2  15427  2lgsoddprmlem3a  15432  2lgsoddprmlem3b  15433  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  ex-fl  15455  ex-exp  15457  ex-fac  15458  ex-bc  15459  ex-dvds  15460  ex-gcd  15461  bj-dfom  15663  012of  15724  2o01f  15725  pwle2  15729  nninfsellemqall  15746  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783  dceqnconst  15791  dcapnconst  15792  taupi  15804