Theorem eqtr4i 1541

Description: An equality transitivity inference.

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 1522	. 2 |- B = C
4	1, 3	eqtri 1538	1 |- A = C

Syntax hints:   = wceq 992

This theorem is referenced by:  3eqtr2i 1544  3eqtr4i 1548  3eqtr4ri 1549  dfin5 2104  dfdif2 2108  difeqri 2212  unrab 2322  inrab 2323  inrab2 2324  difrab 2325  pw0 2532  dfint2 2602  uniiun 2669  intiin 2670  0iin 2674  iunun 2683  dfid3 2914  xpundi 3310  xpundir 3311  rnopab2 3441  resopab 3485  imaundir 3546  cnvcnv 3570  cnvcnv2 3571  cnvcnvres 3592  rnco2 3606  dmco 3607  abrexex2 3985  dmoprab 4062  fnoprv 4077  oprabval4g 4091  oprabval4gALT 4092  1stval2 4150  2ndval2 4151  xp2 4165  dfoprab4s 4176  df1st2 4188  df2nd2 4189  df2o2 4277  o1p1e2 4311  oarec 4332  ecqs 4438  fvopabf4 4481  map0e 4483  ixpconst 4493  ixp0x 4500  1sdom2 4672  abfii4 4707  pwfi 4714  infeq5 4766  rankpr 4838  rankelun 4853  rankelop 4855  kmlem11 4921  cf0 5060  ltexpq 5234  halfpq 5236  genpdm 5259  prlem936a 5307  m1p1sr 5355  m1m1sr 5356  mappsrpr 5372  dfcnqs 5416  ltrecii 6023  lt2msqi 6026  2p2e4 6147  3p2e5 6153  3p3e6 6154  4p2e6 6155  4p3e7 6156  4p4e8 6157  5p2e7 6158  5p3e8 6159  5p4e9 6160  5p5e10 6161  6p2e8 6162  6p3e9 6163  6p4e10 6164  7p2e9 6165  7p3e10 6166  8p2e10 6167  nnzrab 6325  nn0zrab 6326  ioomax 6519  ioopos 6520  ioorp 6521  nn0uz 6565  nnuz 6566  seq1suclem 6681  seq1seqz 6736  seq0seqz 6737  binom2aiOLD 6842  discrlem1 6857  sqrval 6872  sqrlem11 6884  irec 6932  crulem 6937  crmuli 6941  cjcji 6979  cjrebi 6982  cjmuli 6990  addcji 6999  recvalzi 7090  facnn 7136  faclbnd2 7149  faclbnd4lem1 7151  bcpasc2i 7170  serzclim0 7312  isumnn0nn 7411  isumcl 7413  geolimilem 7440  geolim1i 7443  0.999... 7451  cncfval 7469  isupivthi 7495  efcl 7517  efaddlem12 7554  efaddlem20 7562  efaddlem22 7564  eirrlem3 7596  efsepi 7604  ef4pi 7607  sinaddi 7659  cos2OLD 7673  cos1bnd 7683  cos2bnd 7684  efieq1re 7694  ruclem17 7738  infxpidmlem9 7772  alephsuc3 7797  cnconst 7990  cncfmet1 8117  xplm 8186  opr1scn 8191  ablsn 8366  ringsn 8405  nvvop 8475  nvvc 8481  vsfval 8501  nvm 8509  cnims 8581  sqcn 8589  ip1cnilem4 8630  ip1cnilem6 8632  ip0i 8740  ip1ilem 8741  ip2i 8743  ipasslem6 8751  ipasslem7 8752  ipasslem10 8755  minveclem27 8831  pilem3 8940  sinhalfpilem 8946  cospi 8949  sincos6thpi 8979  dflog2 9024  h2hva 9118  h2hsm 9119  h2hvs 9121  h2hcau 9124  h2hlm 9125  axhfvadd 9127  axhvcom 9128  axhvass 9129  axhv0cl 9130  axhvaddid 9131  axhfvmul 9132  axhvmulid 9133  axhvmulass 9134  axhvdistr1 9135  axhvdistr2 9136  axhvmul0 9137  axhfi 9138  axhis1 9139  axhis2 9140  axhis3 9141  axhis4 9142  axhcompl 9143  hvsubassi 9197  normlem0 9251  normlem1 9252  normlem2 9253  normlem4 9255  normlem9 9260  bcseqi 9262  dfhnorm2 9264  normpari 9297  normpar2i 9299  polid2i 9300  polidi 9301  hhba 9310  hhims 9315  hhims2 9316  hhsssh 9415  hhssims 9421  hhssims2 9422  ocval 9429  projlem3 9464  pjthlem1 9495  pjthlem5 9499  pjthlem6 9500  spanval 9575  hsupval2 9576  sshjval 9596  sshjval3 9602  shsumval3i 9637  hosmval 9787  hommval 9788  hodmval 9789  hfsmval 9790  hfmmval 9791  cmcm2i 9812  fh2 9838  qlaxr3i 9855  pjcji 9907  ho0val 9956  df0op2 9958  hosd2i 10029  eigorthi 10043  dfbdop2 10066  hhnmoi 10107  hhbloi 10108  hh0oi 10109  nmop0 10189  nmfn0 10190  lnopeq0lem1 10209  lnophmlem2 10221  nmopcoadji 10313  cvmdi 10532  cdj3lem3 10647  cdj3lem3b 10649  ghomgrpilem2 10671  cayleylem2 10695  infi1 10735  cmpbva 10748  zrdivrng 10969  hmeogrp 11044  stoiglem 11063  clindistop 11131  stoi 11145  trnij 11160  jdmo 11232  compfipin0lem 11492  compfipin0 11493  alexsublem4 11499  ivthALT 11515  neibastop2lem1 11580  extbas2 11642  isufil2 11650  cnvcan 11814  abrexex2g 11825  abrexdom 11826  csbrni 11895  dfii2 11934  constcncf 11944  piececn 11955  bfplem6 12059

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain