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  2798  csb2  3127  cbvrabcsf  3191  difjust  3199  unjust  3201  injust  3203  dfdif3  3315  difeq12i  3321  inrot  3420  symdif1  3470  rabnc  3525  0in  3528  ssdifin0  3574  dfif3  3617  ifbieq2i  3627  ifbieq12i  3629  pwjust  3651  snjust  3672  dfpr2  3686  disjpr2  3731  rabsnifsb  3735  difprsn1  3810  diftpsn3  3812  difpr  3813  dfuni2  3893  intab  3955  intunsn  3964  rint0  3965  iunid  4024  viin  4028  iinrabm  4031  2iunin  4035  riin0  4040  iunxprg  4049  unopab  4166  cbvmptf  4181  cbvmpt  4182  exmid1stab  4296  unisucg  4509  op1stb  4573  orddif  4643  elxpi  4739  csbxpg  4805  relopabi  4853  inxp  4862  coeq12i  4891  dfdm3  4915  dfrn3  4917  dmun  4936  dmopab  4940  dmopab3  4942  dmxpid  4951  dmxpin  4952  rnopab  4977  rnmpt  4978  rncoss  5001  rncoeq  5004  reseq12i  5009  resundi  5024  resindi  5026  resiun1  5030  resdmdfsn  5054  resopab  5055  opabresid  5064  dfima3  5077  mptima  5086  imadisj  5096  ndmima  5111  mptcnv  5137  rnun  5143  rnuni  5146  imaundi  5147  inimass  5151  cnvxp  5153  rnxpm  5164  dminxp  5179  imainrect  5180  cnvcnv3  5184  dmpropg  5207  op1sta  5216  op2ndb  5218  op2nda  5219  resdmres  5226  mptpreima  5228  coundi  5236  coundir  5237  cocnvcnv1  5245  cores2  5247  dfdm2  5269  iotajust  5283  dfiota2  5285  funi  5356  funtp  5380  fntpg  5383  funcnvuni  5396  funcnvres  5400  imadiflem  5406  imadif  5407  imainlem  5408  imain  5409  fnresdisj  5439  mptfng  5455  resdif  5602  fv2  5630  dffv4g  5632  fveq12i  5641  nfvres  5671  0fv  5673  dfimafn2  5691  fnimapr  5702  fvmptss2  5717  fvmptg  5718  fvmpts  5720  fvmpt2  5726  mptfvex  5728  elfvmptrab  5738  fvopab6  5739  f1ompt  5794  dfmpt  5820  ressnop0  5830  fprg  5832  fvsnun1  5846  fsnunfv  5850  fvpr2g  5856  imauni  5897  fliftfuns  5934  cbvriota  5978  oveq123i  6027  fconstmpo  6111  resoprab  6112  mpofun  6118  rnmpo  6127  reldmmpo  6128  ov  6136  ovigg  6137  ovmpt4g  6139  ovg  6156  caov31  6207  elmpocl  6212  f1ocnvd  6220  oprabrexex2  6287  op1st  6304  op2nd  6305  f1stres  6317  f2ndres  6318  unielxp  6332  dfoprab3s  6348  dfoprab4  6350  mpompts  6358  mpofvex  6365  oprab2co  6378  df1st2  6379  df2nd2  6380  f1od2  6395  elmpom  6398  brtpos0  6413  tposoprab  6441  smores3  6454  tfrlemi14d  6494  tfr1onlemaccex  6509  tfrcllemaccex  6522  rdgisuc1  6545  rdg0  6548  frec0g  6558  df1o2  6591  df2o2  6593  oasuc  6627  omv2  6628  omsuc  6635  ecidsn  6746  qliftfuns  6783  oviec  6805  mapsncnv  6859  dfixp  6864  xpcomco  7005  xpassen  7009  ssenen  7032  undifdc  7109  unfiin  7111  fidcenumlemrks  7143  fidcenumlemr  7145  sbthlemi5  7151  sbthlemi8  7154  fi0  7165  inf00  7221  djuf1olemr  7244  djuinr  7253  djuin  7254  djuun  7257  casefun  7275  casedm  7276  caseinj  7279  caseinl  7281  caseinr  7282  endjusym  7286  eninl  7287  eninr  7288  djudm  7295  djuinj  7296  fodjuomni  7339  fodjumkv  7350  nninfwlporlemd  7362  pm54.43  7386  exmidfodomrlemim  7402  xp2dju  7420  djucomen  7421  djuassen  7422  xpdjuen  7423  pw1nel3  7439  sucpw1nel3  7441  addpiord  7526  mulpiord  7527  dmaddpi  7535  dmmulpi  7536  recmulnqg  7601  1lt2nq  7616  halfnqq  7620  dfmq0qs  7639  dfplq0qs  7640  genpdf  7718  1prl  7765  1pru  7766  ltexprlemell  7808  ltexprlemelu  7809  recexprlemell  7832  recexprlemelu  7833  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemupu  7859  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdrl  7867  cauappcvgprlem2  7870  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemupu  7882  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem2  7890  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem2  7920  addsrpr  7955  mulsrpr  7956  caucvgsrlemoffres  8010  caucvgsr  8012  suplocsrlempr  8017  addcnsr  8044  mulcnsr  8045  mulresr  8048  addvalex  8054  pitonnlem1  8055  axi2m1  8085  axcnre  8091  mulcomli  8176  mnfnre  8212  addcomli  8314  add42i  8335  mvrraddi  8386  neg0  8415  negdii  8453  negsubdi2i  8455  crap0  9128  2t2e4  9288  3t2e6  9290  3t3e9  9291  4t2e8  9292  neg1mulneg1e1  9346  8th4div3  9353  halfpm6th  9354  iap0  9357  dfdec10  9604  deceq12i  9609  numltc  9626  decsuc  9631  decsucc  9641  nummac  9645  numma2c  9646  numadd  9647  numaddc  9648  nummul1c  9649  nummul2c  9650  decma  9651  decmac  9652  decma2c  9653  decadd  9654  decaddc  9655  decrmanc  9657  decrmac  9658  decaddci  9661  decsubi  9663  decmul1  9664  decmul1c  9665  decmul2c  9666  11multnc  9668  4t3lem  9697  6t2e12  9704  7t2e14  9709  8t2e16  9715  9t2e18  9722  9t11e99  9730  halfthird  9743  5recm6rec  9744  divfnzn  9845  xnegpnf  10053  xneg0  10056  xaddmnf1  10073  xaddmnf2  10074  mnfaddpnf  10076  iooval2  10140  dfioo2  10199  fzval2  10236  fzsuc2  10304  fztpval  10308  fz0to3un2pr  10348  fz0to4untppr  10349  fzo01  10451  fzo12sn  10452  fzo0to42pr  10455  fldiv4p1lem1div2  10555  intqfrac2  10571  intfracq  10572  xnn0nnen  10689  1tonninf  10693  neg1sqe1  10886  sq2  10887  sq3  10888  cu2  10890  i2  10892  i3  10893  binom2i  10900  sq10  10964  3dec  10966  facp1  10982  fac2  10983  fac4  10985  4bc2eq6  11026  hashp1i  11064  pr0hash2ex  11069  hashfzo  11076  hashxp  11080  zfz1isolem1  11094  elovmpowrd  11145  ccat1st1st  11208  cji  11453  cnrecnv  11461  sqrt0  11555  resqrexlemover  11561  resqrexlemcalc3  11567  absi  11610  absimle  11635  sumeq12i  11916  summodclem2a  11932  summodc  11934  sum0  11939  fsumsplitf  11959  fsum2dlemstep  11985  fsumabs  12016  fsumiun  12028  0.999...  12072  mertenslem2  12087  prodeq12i  12114  prodmodc  12129  fprod2dlemstep  12173  ege2le3  12222  eft0val  12244  cos0  12281  cos1bnd  12310  cos2bnd  12311  3dvdsdec  12416  3dvds2dec  12417  odd2np1  12424  opoe  12446  nn0o  12458  5ndvds3  12485  5ndvds6  12486  bitsfzolem  12505  m1bits  12511  gcd0val  12521  6gcd4e2  12556  nnmindc  12595  nnminle  12596  3lcm2e6woprm  12648  3lcm2e6  12722  nn0gcdsq  12762  phiprmpw  12784  phimullem  12787  pcprecl  12852  pcprendvds  12853  pcmptdvds  12908  pockthi  12921  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  4sqlem19  12972  dec5nprm  12977  dec2nprm  12978  modxai  12979  modsubi  12982  numexp2x  12988  decsplit0b  12989  decsplit0  12990  decsplit  12992  karatsuba  12993  2exp5  12995  2exp7  12997  2exp8  12998  2exp11  12999  2exp16  13000  3exp3  13001  unennn  13008  ennnfonelemj0  13012  ennnfonelem0  13016  ennnfonelem1  13018  ennnfonelemhf1o  13024  ennnfonelemrn  13030  ennnfonelemdm  13031  strnfvnd  13092  slotslfn  13098  setsfun  13107  setsfun0  13108  setscom  13112  setsslid  13123  2strstr1g  13195  eqglact  13802  ecqusaddd  13815  ghmeqker  13848  dfrhm2  14158  rmodislmod  14355  cnfldadd  14566  cnfldmul  14568  expghmap  14611  fczpsrbag  14675  cnco  14935  txuni2  14970  txbas  14972  uptx  14988  txcn  14989  cnmptid  14995  cnmpt2t  15007  xmetxp  15221  cnmetdval  15243  remetdval  15261  resubmet  15270  rerestcntop  15272  rerest  15274  divcnap  15279  cnrehmeocntop  15324  dvexp  15425  plyun0  15450  plyco  15473  plycj  15475  sinhalfpilem  15505  cosneghalfpi  15512  efhalfpi  15513  cospi  15514  efipi  15515  eulerid  15516  sin2pi  15517  cos2pi  15518  ef2pi  15519  sincosq4sgn  15543  cosq14gt0  15546  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  sinkpi  15561  cosq34lt1  15564  dfrelog  15574  2logb9irr  15685  2logb9irrALT  15688  2logb9irrap  15691  mersenne  15711  perfectlem2  15714  zabsle1  15718  lgslem2  15720  lgsfcl2  15725  lgsdir2lem1  15747  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdir2lem5  15751  lgseisen  15793  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgs2  15821  2lgsoddprmlem3a  15826  2lgsoddprmlem3b  15827  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  pw0ss  15924  umgrislfupgrenlem  15969  vtxdgfval  16094  clwwlknon2  16229  clwwlknon2x  16230  ex-fl  16257  ex-exp  16259  ex-fac  16260  ex-bc  16261  ex-dvds  16262  ex-gcd  16263  bj-dfom  16464  012of  16528  2o01f  16529  pwle2  16535  nninfsellemqall  16553  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601  taupi  16613