Theorem eqtri 2226

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtr2i  2227  eqtr3i  2228  eqtr4i  2229  3eqtri  2230  3eqtrri  2231  3eqtr2i  2232  cbvrab  2770  csb2  3095  cbvrabcsf  3159  difjust  3167  unjust  3169  injust  3171  dfdif3  3283  difeq12i  3289  inrot  3388  symdif1  3438  rabnc  3493  0in  3496  ssdifin0  3542  dfif3  3584  ifbieq2i  3594  ifbieq12i  3596  pwjust  3617  snjust  3638  dfpr2  3652  disjpr2  3697  difprsn1  3772  diftpsn3  3774  difpr  3775  dfuni2  3852  intab  3914  intunsn  3923  rint0  3924  iunid  3983  viin  3987  iinrabm  3990  2iunin  3994  riin0  3999  iunxprg  4008  unopab  4123  cbvmptf  4138  cbvmpt  4139  exmid1stab  4252  unisucg  4461  op1stb  4525  orddif  4595  elxpi  4691  csbxpg  4756  relopabi  4803  inxp  4812  coeq12i  4841  dfdm3  4865  dfrn3  4867  dmun  4885  dmopab  4889  dmopab3  4891  dmxpid  4899  dmxpin  4900  rnopab  4925  rnmpt  4926  rncoss  4949  rncoeq  4952  reseq12i  4957  resundi  4972  resindi  4974  resiun1  4978  resdmdfsn  5002  resopab  5003  opabresid  5012  dfima3  5025  mptima  5034  imadisj  5044  ndmima  5059  mptcnv  5085  rnun  5091  rnuni  5094  imaundi  5095  inimass  5099  cnvxp  5101  rnxpm  5112  dminxp  5127  imainrect  5128  cnvcnv3  5132  dmpropg  5155  op1sta  5164  op2ndb  5166  op2nda  5167  resdmres  5174  mptpreima  5176  coundi  5184  coundir  5185  cocnvcnv1  5193  cores2  5195  dfdm2  5217  iotajust  5231  dfiota2  5233  funi  5303  funtp  5327  fntpg  5330  funcnvuni  5343  funcnvres  5347  imadiflem  5353  imadif  5354  imainlem  5355  imain  5356  fnresdisj  5386  mptfng  5401  resdif  5544  fv2  5571  dffv4g  5573  fveq12i  5582  nfvres  5610  0fv  5612  dfimafn2  5628  fnimapr  5639  fvmptss2  5654  fvmptg  5655  fvmpts  5657  fvmpt2  5663  mptfvex  5665  elfvmptrab  5675  fvopab6  5676  f1ompt  5731  dfmpt  5757  ressnop0  5765  fprg  5767  fvsnun1  5781  fsnunfv  5785  fvpr2g  5791  imauni  5830  fliftfuns  5867  cbvriota  5910  oveq123i  5958  fconstmpo  6040  resoprab  6041  mpofun  6047  rnmpo  6056  reldmmpo  6057  ov  6065  ovigg  6066  ovmpt4g  6068  ovg  6085  caov31  6136  elmpocl  6141  f1ocnvd  6148  oprabrexex2  6215  op1st  6232  op2nd  6233  f1stres  6245  f2ndres  6246  unielxp  6260  dfoprab3s  6276  dfoprab4  6278  mpompts  6284  mpofvex  6291  oprab2co  6304  df1st2  6305  df2nd2  6306  f1od2  6321  brtpos0  6338  tposoprab  6366  smores3  6379  tfrlemi14d  6419  tfr1onlemaccex  6434  tfrcllemaccex  6447  rdgisuc1  6470  rdg0  6473  frec0g  6483  df1o2  6515  df2o2  6517  oasuc  6550  omv2  6551  omsuc  6558  ecidsn  6669  qliftfuns  6706  oviec  6728  mapsncnv  6782  dfixp  6787  xpcomco  6921  xpassen  6925  ssenen  6948  undifdc  7021  unfiin  7023  fidcenumlemrks  7055  fidcenumlemr  7057  sbthlemi5  7063  sbthlemi8  7066  fi0  7077  inf00  7133  djuf1olemr  7156  djuinr  7165  djuin  7166  djuun  7169  casefun  7187  casedm  7188  caseinj  7191  caseinl  7193  caseinr  7194  endjusym  7198  eninl  7199  eninr  7200  djudm  7207  djuinj  7208  fodjuomni  7251  fodjumkv  7262  nninfwlporlemd  7274  pm54.43  7298  exmidfodomrlemim  7309  xp2dju  7327  djucomen  7328  djuassen  7329  xpdjuen  7330  pw1nel3  7343  sucpw1nel3  7345  addpiord  7429  mulpiord  7430  dmaddpi  7438  dmmulpi  7439  recmulnqg  7504  1lt2nq  7519  halfnqq  7523  dfmq0qs  7542  dfplq0qs  7543  genpdf  7621  1prl  7668  1pru  7669  ltexprlemell  7711  ltexprlemelu  7712  recexprlemell  7735  recexprlemelu  7736  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdrl  7770  cauappcvgprlem2  7773  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem2  7793  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem2  7823  addsrpr  7858  mulsrpr  7859  caucvgsrlemoffres  7913  caucvgsr  7915  suplocsrlempr  7920  addcnsr  7947  mulcnsr  7948  mulresr  7951  addvalex  7957  pitonnlem1  7958  axi2m1  7988  axcnre  7994  mulcomli  8079  mnfnre  8115  addcomli  8217  add42i  8238  mvrraddi  8289  neg0  8318  negdii  8356  negsubdi2i  8358  crap0  9031  2t2e4  9191  3t2e6  9193  3t3e9  9194  4t2e8  9195  neg1mulneg1e1  9249  8th4div3  9256  halfpm6th  9257  iap0  9260  dfdec10  9507  deceq12i  9512  numltc  9529  decsuc  9534  decsucc  9544  nummac  9548  numma2c  9549  numadd  9550  numaddc  9551  nummul1c  9552  nummul2c  9553  decma  9554  decmac  9555  decma2c  9556  decadd  9557  decaddc  9558  decrmanc  9560  decrmac  9561  decaddci  9564  decsubi  9566  decmul1  9567  decmul1c  9568  decmul2c  9569  11multnc  9571  4t3lem  9600  6t2e12  9607  7t2e14  9612  8t2e16  9618  9t2e18  9625  9t11e99  9633  halfthird  9646  5recm6rec  9647  divfnzn  9742  xnegpnf  9950  xneg0  9953  xaddmnf1  9970  xaddmnf2  9971  mnfaddpnf  9973  iooval2  10037  dfioo2  10096  fzval2  10133  fzsuc2  10201  fztpval  10205  fz0to3un2pr  10245  fz0to4untppr  10246  fzo01  10345  fzo12sn  10346  fzo0to42pr  10349  fldiv4p1lem1div2  10448  intqfrac2  10464  intfracq  10465  xnn0nnen  10582  1tonninf  10586  neg1sqe1  10779  sq2  10780  sq3  10781  cu2  10783  i2  10785  i3  10786  binom2i  10793  sq10  10857  3dec  10859  facp1  10875  fac2  10876  fac4  10878  4bc2eq6  10919  hashp1i  10955  pr0hash2ex  10960  hashfzo  10967  hashxp  10971  zfz1isolem1  10985  elovmpowrd  11035  ccat1st1st  11093  cji  11213  cnrecnv  11221  sqrt0  11315  resqrexlemover  11321  resqrexlemcalc3  11327  absi  11370  absimle  11395  sumeq12i  11676  summodclem2a  11692  summodc  11694  sum0  11699  fsumsplitf  11719  fsum2dlemstep  11745  fsumabs  11776  fsumiun  11788  0.999...  11832  mertenslem2  11847  prodeq12i  11874  prodmodc  11889  fprod2dlemstep  11933  ege2le3  11982  eft0val  12004  cos0  12041  cos1bnd  12070  cos2bnd  12071  3dvdsdec  12176  3dvds2dec  12177  odd2np1  12184  opoe  12206  nn0o  12218  5ndvds3  12245  5ndvds6  12246  bitsfzolem  12265  m1bits  12271  gcd0val  12281  6gcd4e2  12316  nnmindc  12355  nnminle  12356  3lcm2e6woprm  12408  3lcm2e6  12482  nn0gcdsq  12522  phiprmpw  12544  phimullem  12547  pcprecl  12612  pcprendvds  12613  pcmptdvds  12668  pockthi  12681  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  4sqlem19  12732  dec5nprm  12737  dec2nprm  12738  modxai  12739  modsubi  12742  numexp2x  12748  decsplit0b  12749  decsplit0  12750  decsplit  12752  karatsuba  12753  2exp5  12755  2exp7  12757  2exp8  12758  2exp11  12759  2exp16  12760  3exp3  12761  unennn  12768  ennnfonelemj0  12772  ennnfonelem0  12776  ennnfonelem1  12778  ennnfonelemhf1o  12784  ennnfonelemrn  12790  ennnfonelemdm  12791  strnfvnd  12852  slotslfn  12858  setsfun  12867  setsfun0  12868  setscom  12872  setsslid  12883  2strstr1g  12954  eqglact  13561  ecqusaddd  13574  ghmeqker  13607  dfrhm2  13916  rmodislmod  14113  cnfldadd  14324  cnfldmul  14326  expghmap  14369  fczpsrbag  14433  cnco  14693  txuni2  14728  txbas  14730  uptx  14746  txcn  14747  cnmptid  14753  cnmpt2t  14765  xmetxp  14979  cnmetdval  15001  remetdval  15019  resubmet  15028  rerestcntop  15030  rerest  15032  divcnap  15037  cnrehmeocntop  15082  dvexp  15183  plyun0  15208  plyco  15231  plycj  15233  sinhalfpilem  15263  cosneghalfpi  15270  efhalfpi  15271  cospi  15272  efipi  15273  eulerid  15274  sin2pi  15275  cos2pi  15276  ef2pi  15277  sincosq4sgn  15301  cosq14gt0  15304  tangtx  15310  sincos4thpi  15312  sincos6thpi  15314  sinkpi  15319  cosq34lt1  15322  dfrelog  15332  2logb9irr  15443  2logb9irrALT  15446  2logb9irrap  15449  mersenne  15469  perfectlem2  15472  zabsle1  15476  lgslem2  15478  lgsfcl2  15483  lgsdir2lem1  15505  lgsdir2lem2  15506  lgsdir2lem4  15508  lgsdir2lem5  15509  lgseisen  15551  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgs2  15579  2lgsoddprmlem3a  15584  2lgsoddprmlem3b  15585  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587  ex-fl  15661  ex-exp  15663  ex-fac  15664  ex-bc  15665  ex-dvds  15666  ex-gcd  15667  bj-dfom  15869  012of  15930  2o01f  15931  pwle2  15935  nninfsellemqall  15952  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991  dceqnconst  15999  dcapnconst  16000  taupi  16012