Theorem eqtri 2250

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  3eqtri  2254  3eqtrri  2255  3eqtr2i  2256  cbvrab  2797  csb2  3126  cbvrabcsf  3190  difjust  3198  unjust  3200  injust  3202  dfdif3  3314  difeq12i  3320  inrot  3419  symdif1  3469  rabnc  3524  0in  3527  ssdifin0  3573  dfif3  3616  ifbieq2i  3626  ifbieq12i  3628  pwjust  3650  snjust  3671  dfpr2  3685  disjpr2  3730  difprsn1  3807  diftpsn3  3809  difpr  3810  dfuni2  3890  intab  3952  intunsn  3961  rint0  3962  iunid  4021  viin  4025  iinrabm  4028  2iunin  4032  riin0  4037  iunxprg  4046  unopab  4163  cbvmptf  4178  cbvmpt  4179  exmid1stab  4292  unisucg  4505  op1stb  4569  orddif  4639  elxpi  4735  csbxpg  4800  relopabi  4847  inxp  4856  coeq12i  4885  dfdm3  4909  dfrn3  4911  dmun  4930  dmopab  4934  dmopab3  4936  dmxpid  4945  dmxpin  4946  rnopab  4971  rnmpt  4972  rncoss  4995  rncoeq  4998  reseq12i  5003  resundi  5018  resindi  5020  resiun1  5024  resdmdfsn  5048  resopab  5049  opabresid  5058  dfima3  5071  mptima  5080  imadisj  5090  ndmima  5105  mptcnv  5131  rnun  5137  rnuni  5140  imaundi  5141  inimass  5145  cnvxp  5147  rnxpm  5158  dminxp  5173  imainrect  5174  cnvcnv3  5178  dmpropg  5201  op1sta  5210  op2ndb  5212  op2nda  5213  resdmres  5220  mptpreima  5222  coundi  5230  coundir  5231  cocnvcnv1  5239  cores2  5241  dfdm2  5263  iotajust  5277  dfiota2  5279  funi  5350  funtp  5374  fntpg  5377  funcnvuni  5390  funcnvres  5394  imadiflem  5400  imadif  5401  imainlem  5402  imain  5403  fnresdisj  5433  mptfng  5449  resdif  5596  fv2  5624  dffv4g  5626  fveq12i  5635  nfvres  5665  0fv  5667  dfimafn2  5685  fnimapr  5696  fvmptss2  5711  fvmptg  5712  fvmpts  5714  fvmpt2  5720  mptfvex  5722  elfvmptrab  5732  fvopab6  5733  f1ompt  5788  dfmpt  5814  ressnop0  5824  fprg  5826  fvsnun1  5840  fsnunfv  5844  fvpr2g  5850  imauni  5891  fliftfuns  5928  cbvriota  5972  oveq123i  6021  fconstmpo  6105  resoprab  6106  mpofun  6112  rnmpo  6121  reldmmpo  6122  ov  6130  ovigg  6131  ovmpt4g  6133  ovg  6150  caov31  6201  elmpocl  6206  f1ocnvd  6214  oprabrexex2  6281  op1st  6298  op2nd  6299  f1stres  6311  f2ndres  6312  unielxp  6326  dfoprab3s  6342  dfoprab4  6344  mpompts  6350  mpofvex  6357  oprab2co  6370  df1st2  6371  df2nd2  6372  f1od2  6387  brtpos0  6404  tposoprab  6432  smores3  6445  tfrlemi14d  6485  tfr1onlemaccex  6500  tfrcllemaccex  6513  rdgisuc1  6536  rdg0  6539  frec0g  6549  df1o2  6582  df2o2  6584  oasuc  6618  omv2  6619  omsuc  6626  ecidsn  6737  qliftfuns  6774  oviec  6796  mapsncnv  6850  dfixp  6855  xpcomco  6993  xpassen  6997  ssenen  7020  undifdc  7097  unfiin  7099  fidcenumlemrks  7131  fidcenumlemr  7133  sbthlemi5  7139  sbthlemi8  7142  fi0  7153  inf00  7209  djuf1olemr  7232  djuinr  7241  djuin  7242  djuun  7245  casefun  7263  casedm  7264  caseinj  7267  caseinl  7269  caseinr  7270  endjusym  7274  eninl  7275  eninr  7276  djudm  7283  djuinj  7284  fodjuomni  7327  fodjumkv  7338  nninfwlporlemd  7350  pm54.43  7374  exmidfodomrlemim  7390  xp2dju  7408  djucomen  7409  djuassen  7410  xpdjuen  7411  pw1nel3  7427  sucpw1nel3  7429  addpiord  7514  mulpiord  7515  dmaddpi  7523  dmmulpi  7524  recmulnqg  7589  1lt2nq  7604  halfnqq  7608  dfmq0qs  7627  dfplq0qs  7628  genpdf  7706  1prl  7753  1pru  7754  ltexprlemell  7796  ltexprlemelu  7797  recexprlemell  7820  recexprlemelu  7821  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem2  7878  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem2  7908  addsrpr  7943  mulsrpr  7944  caucvgsrlemoffres  7998  caucvgsr  8000  suplocsrlempr  8005  addcnsr  8032  mulcnsr  8033  mulresr  8036  addvalex  8042  pitonnlem1  8043  axi2m1  8073  axcnre  8079  mulcomli  8164  mnfnre  8200  addcomli  8302  add42i  8323  mvrraddi  8374  neg0  8403  negdii  8441  negsubdi2i  8443  crap0  9116  2t2e4  9276  3t2e6  9278  3t3e9  9279  4t2e8  9280  neg1mulneg1e1  9334  8th4div3  9341  halfpm6th  9342  iap0  9345  dfdec10  9592  deceq12i  9597  numltc  9614  decsuc  9619  decsucc  9629  nummac  9633  numma2c  9634  numadd  9635  numaddc  9636  nummul1c  9637  nummul2c  9638  decma  9639  decmac  9640  decma2c  9641  decadd  9642  decaddc  9643  decrmanc  9645  decrmac  9646  decaddci  9649  decsubi  9651  decmul1  9652  decmul1c  9653  decmul2c  9654  11multnc  9656  4t3lem  9685  6t2e12  9692  7t2e14  9697  8t2e16  9703  9t2e18  9710  9t11e99  9718  halfthird  9731  5recm6rec  9732  divfnzn  9828  xnegpnf  10036  xneg0  10039  xaddmnf1  10056  xaddmnf2  10057  mnfaddpnf  10059  iooval2  10123  dfioo2  10182  fzval2  10219  fzsuc2  10287  fztpval  10291  fz0to3un2pr  10331  fz0to4untppr  10332  fzo01  10434  fzo12sn  10435  fzo0to42pr  10438  fldiv4p1lem1div2  10537  intqfrac2  10553  intfracq  10554  xnn0nnen  10671  1tonninf  10675  neg1sqe1  10868  sq2  10869  sq3  10870  cu2  10872  i2  10874  i3  10875  binom2i  10882  sq10  10946  3dec  10948  facp1  10964  fac2  10965  fac4  10967  4bc2eq6  11008  hashp1i  11045  pr0hash2ex  11050  hashfzo  11057  hashxp  11061  zfz1isolem1  11075  elovmpowrd  11126  ccat1st1st  11187  cji  11428  cnrecnv  11436  sqrt0  11530  resqrexlemover  11536  resqrexlemcalc3  11542  absi  11585  absimle  11610  sumeq12i  11891  summodclem2a  11907  summodc  11909  sum0  11914  fsumsplitf  11934  fsum2dlemstep  11960  fsumabs  11991  fsumiun  12003  0.999...  12047  mertenslem2  12062  prodeq12i  12089  prodmodc  12104  fprod2dlemstep  12148  ege2le3  12197  eft0val  12219  cos0  12256  cos1bnd  12285  cos2bnd  12286  3dvdsdec  12391  3dvds2dec  12392  odd2np1  12399  opoe  12421  nn0o  12433  5ndvds3  12460  5ndvds6  12461  bitsfzolem  12480  m1bits  12486  gcd0val  12496  6gcd4e2  12531  nnmindc  12570  nnminle  12571  3lcm2e6woprm  12623  3lcm2e6  12697  nn0gcdsq  12737  phiprmpw  12759  phimullem  12762  pcprecl  12827  pcprendvds  12828  pcmptdvds  12883  pockthi  12896  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  4sqlem18  12946  4sqlem19  12947  dec5nprm  12952  dec2nprm  12953  modxai  12954  modsubi  12957  numexp2x  12963  decsplit0b  12964  decsplit0  12965  decsplit  12967  karatsuba  12968  2exp5  12970  2exp7  12972  2exp8  12973  2exp11  12974  2exp16  12975  3exp3  12976  unennn  12983  ennnfonelemj0  12987  ennnfonelem0  12991  ennnfonelem1  12993  ennnfonelemhf1o  12999  ennnfonelemrn  13005  ennnfonelemdm  13006  strnfvnd  13067  slotslfn  13073  setsfun  13082  setsfun0  13083  setscom  13087  setsslid  13098  2strstr1g  13170  eqglact  13777  ecqusaddd  13790  ghmeqker  13823  dfrhm2  14133  rmodislmod  14330  cnfldadd  14541  cnfldmul  14543  expghmap  14586  fczpsrbag  14650  cnco  14910  txuni2  14945  txbas  14947  uptx  14963  txcn  14964  cnmptid  14970  cnmpt2t  14982  xmetxp  15196  cnmetdval  15218  remetdval  15236  resubmet  15245  rerestcntop  15247  rerest  15249  divcnap  15254  cnrehmeocntop  15299  dvexp  15400  plyun0  15425  plyco  15448  plycj  15450  sinhalfpilem  15480  cosneghalfpi  15487  efhalfpi  15488  cospi  15489  efipi  15490  eulerid  15491  sin2pi  15492  cos2pi  15493  ef2pi  15494  sincosq4sgn  15518  cosq14gt0  15521  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  sinkpi  15536  cosq34lt1  15539  dfrelog  15549  2logb9irr  15660  2logb9irrALT  15663  2logb9irrap  15666  mersenne  15686  perfectlem2  15689  zabsle1  15693  lgslem2  15695  lgsfcl2  15700  lgsdir2lem1  15722  lgsdir2lem2  15723  lgsdir2lem4  15725  lgsdir2lem5  15726  lgseisen  15768  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgs2  15796  2lgsoddprmlem3a  15801  2lgsoddprmlem3b  15802  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  pw0ss  15898  umgrislfupgrenlem  15943  vtxdgfval  16047  ex-fl  16148  ex-exp  16150  ex-fac  16151  ex-bc  16152  ex-dvds  16153  ex-gcd  16154  bj-dfom  16355  012of  16420  2o01f  16421  pwle2  16427  nninfsellemqall  16445  isomninnlem  16462  iswomninnlem  16481  ismkvnnlem  16484  dceqnconst  16492  dcapnconst  16493  taupi  16505