Theorem eqtr4i 2231

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	|- A = B
eqtr4i.2	|- C = B

Assertion

Ref	Expression
eqtr4i	|- A = C

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 |- A = B
2		eqtr4i.2	. . 3 |- C = B
3	2	eqcomi 2211	. 2 |- B = C
4	1, 3	eqtri 2228	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtr2i  2234  3eqtr2ri  2235  3eqtr4i  2238  3eqtr4ri  2239  rabab  2798  cbvralcsf  3164  cbvrexcsf  3165  cbvrabcsf  3167  dfin5  3181  dfdif2  3182  uneqin  3432  unrab  3452  inrab  3453  inrab2  3454  difrab  3455  dfrab3ss  3459  rabun2  3460  difidALT  3538  difdifdirss  3553  dfif3  3593  tpidm  3745  dfint2  3901  iunrab  3989  uniiun  3995  intiin  3996  0iin  4000  mptv  4157  xpundi  4749  xpundir  4750  resiun2  4998  resopab  5022  mptresid  5032  dfse2  5074  cnvun  5107  cnvin  5109  imaundir  5115  imainrect  5147  cnvcnv2  5155  cnvcnvres  5165  dmtpop  5177  rnsnopg  5180  rnco2  5209  dmco  5210  co01  5216  unidmrn  5234  dfdm2  5236  funimaexg  5377  dfmpt3  5418  mptun  5427  funcocnv2  5569  fnasrn  5781  fnasrng  5783  fpr  5789  fmptap  5797  riotav  5928  dmoprab  6049  rnoprab2  6052  mpov  6058  mpomptx  6059  abrexex2g  6228  abrexex2  6232  1stval2  6264  2ndval2  6265  fo1st  6266  fo2nd  6267  xp2  6282  dfoprab4f  6302  fmpoco  6325  tposmpo  6390  recsfval  6424  frecfnom  6510  freccllem  6511  frecfcllem  6513  frecsuclem  6515  df2o3  6539  o1p1e2  6577  ecqs  6707  qliftf  6730  erovlem  6737  mapsnf1o3  6807  ixp0x  6836  xpf1o  6966  djuunr  7194  dmaddpq  7527  dmmulpq  7528  enq0enq  7579  nqprlu  7695  m1p1sr  7908  m1m1sr  7909  caucvgsr  7950  dfcnqs  7989  3m1e2  9191  2p2e4  9198  3p2e5  9213  3p3e6  9214  4p2e6  9215  4p3e7  9216  4p4e8  9217  5p2e7  9218  5p3e8  9219  5p4e9  9220  6p2e8  9221  6p3e9  9222  7p2e9  9223  nn0supp  9382  nnzrab  9431  nn0zrab  9432  dec0u  9559  dec0h  9560  decsuc  9569  decsucc  9579  numma  9582  decma  9589  decmac  9590  decma2c  9591  decadd  9592  decaddc  9593  decmul1  9602  decmul1c  9603  decmul2c  9604  5p5e10  9609  6p4e10  9610  7p3e10  9613  8p2e10  9618  5t5e25  9641  6t6e36  9646  8t6e48  9657  nn0uz  9718  nnuz  9719  xaddcom  10018  ioomax  10105  iccmax  10106  ioopos  10107  ioorp  10108  fseq1p1m1  10251  fzo0to2pr  10384  fzo0to3tp  10385  frecfzennn  10608  irec  10821  sq10e99m1  10895  facnn  10909  fac0  10910  faclbnd2  10924  zfz1isolemsplit  11020  minmax  11656  xrminmax  11691  fisumrev2  11872  fsumparts  11896  fsumiun  11903  isumnn0nn  11919  fprod2d  12049  fprodle  12066  ege2le3  12097  cos1bnd  12185  efieq1re  12198  eirraplem  12203  3dvds  12290  m1bits  12386  phiprmpw  12659  4sqlem11  12839  4sqlem19  12847  dec5dvds  12850  decsplit1  12866  unennn  12883  ennnfonelemjn  12888  qnnen  12917  strle1g  13053  quslem  13271  rmodislmod  14228  tgrest  14756  uniretop  15112  cnfldtopn  15126  dvexp  15298  dvef  15314  elply2  15322  cospi  15387  sincos6thpi  15429  lgsdir2lem2  15621  lgsquadlem2  15670  lgsquad2lem2  15674  2lgsoddprmlem3c  15701  bj-omind  16069