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  3806  diftpsn3  3808  difpr  3809  dfuni2  3889  intab  3951  intunsn  3960  rint0  3961  iunid  4020  viin  4024  iinrabm  4027  2iunin  4031  riin0  4036  iunxprg  4045  unopab  4162  cbvmptf  4177  cbvmpt  4178  exmid1stab  4291  unisucg  4504  op1stb  4568  orddif  4638  elxpi  4734  csbxpg  4799  relopabi  4846  inxp  4855  coeq12i  4884  dfdm3  4908  dfrn3  4910  dmun  4929  dmopab  4933  dmopab3  4935  dmxpid  4944  dmxpin  4945  rnopab  4970  rnmpt  4971  rncoss  4994  rncoeq  4997  reseq12i  5002  resundi  5017  resindi  5019  resiun1  5023  resdmdfsn  5047  resopab  5048  opabresid  5057  dfima3  5070  mptima  5079  imadisj  5089  ndmima  5104  mptcnv  5130  rnun  5136  rnuni  5139  imaundi  5140  inimass  5144  cnvxp  5146  rnxpm  5157  dminxp  5172  imainrect  5173  cnvcnv3  5177  dmpropg  5200  op1sta  5209  op2ndb  5211  op2nda  5212  resdmres  5219  mptpreima  5221  coundi  5229  coundir  5230  cocnvcnv1  5238  cores2  5240  dfdm2  5262  iotajust  5276  dfiota2  5278  funi  5349  funtp  5373  fntpg  5376  funcnvuni  5389  funcnvres  5393  imadiflem  5399  imadif  5400  imainlem  5401  imain  5402  fnresdisj  5432  mptfng  5448  resdif  5593  fv2  5621  dffv4g  5623  fveq12i  5632  nfvres  5662  0fv  5664  dfimafn2  5682  fnimapr  5693  fvmptss2  5708  fvmptg  5709  fvmpts  5711  fvmpt2  5717  mptfvex  5719  elfvmptrab  5729  fvopab6  5730  f1ompt  5785  dfmpt  5811  ressnop0  5819  fprg  5821  fvsnun1  5835  fsnunfv  5839  fvpr2g  5845  imauni  5884  fliftfuns  5921  cbvriota  5965  oveq123i  6014  fconstmpo  6098  resoprab  6099  mpofun  6105  rnmpo  6114  reldmmpo  6115  ov  6123  ovigg  6124  ovmpt4g  6126  ovg  6143  caov31  6194  elmpocl  6199  f1ocnvd  6206  oprabrexex2  6273  op1st  6290  op2nd  6291  f1stres  6303  f2ndres  6304  unielxp  6318  dfoprab3s  6334  dfoprab4  6336  mpompts  6342  mpofvex  6349  oprab2co  6362  df1st2  6363  df2nd2  6364  f1od2  6379  brtpos0  6396  tposoprab  6424  smores3  6437  tfrlemi14d  6477  tfr1onlemaccex  6492  tfrcllemaccex  6505  rdgisuc1  6528  rdg0  6531  frec0g  6541  df1o2  6573  df2o2  6575  oasuc  6608  omv2  6609  omsuc  6616  ecidsn  6727  qliftfuns  6764  oviec  6786  mapsncnv  6840  dfixp  6845  xpcomco  6981  xpassen  6985  ssenen  7008  undifdc  7082  unfiin  7084  fidcenumlemrks  7116  fidcenumlemr  7118  sbthlemi5  7124  sbthlemi8  7127  fi0  7138  inf00  7194  djuf1olemr  7217  djuinr  7226  djuin  7227  djuun  7230  casefun  7248  casedm  7249  caseinj  7252  caseinl  7254  caseinr  7255  endjusym  7259  eninl  7260  eninr  7261  djudm  7268  djuinj  7269  fodjuomni  7312  fodjumkv  7323  nninfwlporlemd  7335  pm54.43  7359  exmidfodomrlemim  7375  xp2dju  7393  djucomen  7394  djuassen  7395  xpdjuen  7396  pw1nel3  7412  sucpw1nel3  7414  addpiord  7499  mulpiord  7500  dmaddpi  7508  dmmulpi  7509  recmulnqg  7574  1lt2nq  7589  halfnqq  7593  dfmq0qs  7612  dfplq0qs  7613  genpdf  7691  1prl  7738  1pru  7739  ltexprlemell  7781  ltexprlemelu  7782  recexprlemell  7805  recexprlemelu  7806  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdrl  7840  cauappcvgprlem2  7843  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem2  7863  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem2  7893  addsrpr  7928  mulsrpr  7929  caucvgsrlemoffres  7983  caucvgsr  7985  suplocsrlempr  7990  addcnsr  8017  mulcnsr  8018  mulresr  8021  addvalex  8027  pitonnlem1  8028  axi2m1  8058  axcnre  8064  mulcomli  8149  mnfnre  8185  addcomli  8287  add42i  8308  mvrraddi  8359  neg0  8388  negdii  8426  negsubdi2i  8428  crap0  9101  2t2e4  9261  3t2e6  9263  3t3e9  9264  4t2e8  9265  neg1mulneg1e1  9319  8th4div3  9326  halfpm6th  9327  iap0  9330  dfdec10  9577  deceq12i  9582  numltc  9599  decsuc  9604  decsucc  9614  nummac  9618  numma2c  9619  numadd  9620  numaddc  9621  nummul1c  9622  nummul2c  9623  decma  9624  decmac  9625  decma2c  9626  decadd  9627  decaddc  9628  decrmanc  9630  decrmac  9631  decaddci  9634  decsubi  9636  decmul1  9637  decmul1c  9638  decmul2c  9639  11multnc  9641  4t3lem  9670  6t2e12  9677  7t2e14  9682  8t2e16  9688  9t2e18  9695  9t11e99  9703  halfthird  9716  5recm6rec  9717  divfnzn  9812  xnegpnf  10020  xneg0  10023  xaddmnf1  10040  xaddmnf2  10041  mnfaddpnf  10043  iooval2  10107  dfioo2  10166  fzval2  10203  fzsuc2  10271  fztpval  10275  fz0to3un2pr  10315  fz0to4untppr  10316  fzo01  10417  fzo12sn  10418  fzo0to42pr  10421  fldiv4p1lem1div2  10520  intqfrac2  10536  intfracq  10537  xnn0nnen  10654  1tonninf  10658  neg1sqe1  10851  sq2  10852  sq3  10853  cu2  10855  i2  10857  i3  10858  binom2i  10865  sq10  10929  3dec  10931  facp1  10947  fac2  10948  fac4  10950  4bc2eq6  10991  hashp1i  11027  pr0hash2ex  11032  hashfzo  11039  hashxp  11043  zfz1isolem1  11057  elovmpowrd  11108  ccat1st1st  11167  cji  11408  cnrecnv  11416  sqrt0  11510  resqrexlemover  11516  resqrexlemcalc3  11522  absi  11565  absimle  11590  sumeq12i  11871  summodclem2a  11887  summodc  11889  sum0  11894  fsumsplitf  11914  fsum2dlemstep  11940  fsumabs  11971  fsumiun  11983  0.999...  12027  mertenslem2  12042  prodeq12i  12069  prodmodc  12084  fprod2dlemstep  12128  ege2le3  12177  eft0val  12199  cos0  12236  cos1bnd  12265  cos2bnd  12266  3dvdsdec  12371  3dvds2dec  12372  odd2np1  12379  opoe  12401  nn0o  12413  5ndvds3  12440  5ndvds6  12441  bitsfzolem  12460  m1bits  12466  gcd0val  12476  6gcd4e2  12511  nnmindc  12550  nnminle  12551  3lcm2e6woprm  12603  3lcm2e6  12677  nn0gcdsq  12717  phiprmpw  12739  phimullem  12742  pcprecl  12807  pcprendvds  12808  pcmptdvds  12863  pockthi  12876  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  4sqlem19  12927  dec5nprm  12932  dec2nprm  12933  modxai  12934  modsubi  12937  numexp2x  12943  decsplit0b  12944  decsplit0  12945  decsplit  12947  karatsuba  12948  2exp5  12950  2exp7  12952  2exp8  12953  2exp11  12954  2exp16  12955  3exp3  12956  unennn  12963  ennnfonelemj0  12967  ennnfonelem0  12971  ennnfonelem1  12973  ennnfonelemhf1o  12979  ennnfonelemrn  12985  ennnfonelemdm  12986  strnfvnd  13047  slotslfn  13053  setsfun  13062  setsfun0  13063  setscom  13067  setsslid  13078  2strstr1g  13150  eqglact  13757  ecqusaddd  13770  ghmeqker  13803  dfrhm2  14112  rmodislmod  14309  cnfldadd  14520  cnfldmul  14522  expghmap  14565  fczpsrbag  14629  cnco  14889  txuni2  14924  txbas  14926  uptx  14942  txcn  14943  cnmptid  14949  cnmpt2t  14961  xmetxp  15175  cnmetdval  15197  remetdval  15215  resubmet  15224  rerestcntop  15226  rerest  15228  divcnap  15233  cnrehmeocntop  15278  dvexp  15379  plyun0  15404  plyco  15427  plycj  15429  sinhalfpilem  15459  cosneghalfpi  15466  efhalfpi  15467  cospi  15468  efipi  15469  eulerid  15470  sin2pi  15471  cos2pi  15472  ef2pi  15473  sincosq4sgn  15497  cosq14gt0  15500  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  sinkpi  15515  cosq34lt1  15518  dfrelog  15528  2logb9irr  15639  2logb9irrALT  15642  2logb9irrap  15645  mersenne  15665  perfectlem2  15668  zabsle1  15672  lgslem2  15674  lgsfcl2  15679  lgsdir2lem1  15701  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdir2lem5  15705  lgseisen  15747  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgs2  15775  2lgsoddprmlem3a  15780  2lgsoddprmlem3b  15781  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  pw0ss  15877  umgrislfupgrenlem  15922  ex-fl  16047  ex-exp  16049  ex-fac  16050  ex-bc  16051  ex-dvds  16052  ex-gcd  16053  bj-dfom  16254  012of  16316  2o01f  16317  pwle2  16323  nninfsellemqall  16340  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379  dceqnconst  16387  dcapnconst  16388  taupi  16400