Theorem eqtr4 1496

Description: An equality transitivity inference.

Hypotheses

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

Assertion

Ref	Expression
eqtr4	|- A = C

Proof of Theorem eqtr4

Step	Hyp	Ref	Expression
1		eqtr4.1	. 2 |- A = B
2		eqtr4.2	. . 3 |- C = B
3	2	eqcomi 1477	. 2 |- B = C
4	1, 3	eqtr 1493	1 |- A = C

Syntax hints:   = wceq 955

This theorem is referenced by:  3eqtr2 1499  3eqtr4 1503  3eqtr4r 1504  dfin5 2049  dfdif2 2053  difeqri 2157  unrab 2267  inrab 2268  inrab2 2269  difrab 2270  pw0 2465  dfint2 2531  uniiun 2597  intiin 2598  0iin 2602  iunun 2609  dfid3 2832  xpundi 3221  xpundir 3222  rnopab2 3350  resopab 3391  imaun2 3457  cnvcnv 3482  cnvcnv2 3483  cnvcnvres 3490  rnco2 3499  dmco2 3500  abrexex2 3866  dmoprab 3997  fnoprval 4012  oprabval4g 4026  1stval2 4082  2ndval2 4083  xp2 4098  df1st2 4119  df2nd2 4120  df2o2 4134  o1p1e2 4168  oarec 4189  fvopabf4 4333  map0e 4335  ixpconst 4345  ixp0x 4352  1sdom2 4514  abfii4 4547  pwfi 4554  infeq5 4604  rankpr 4675  rankelun 4690  rankelop 4692  kmlem11 4758  cf0 4893  ltexpq 5063  halfpq 5065  genpdm 5088  prlem936a 5136  m1p1sr 5184  m1m1sr 5185  mappsrpr 5201  dfcnqs 5245  ltreci 5836  lt2msq 5839  2p2e4 5958  3p2e5 5964  3p3e6 5965  4p2e6 5966  4p3e7 5967  4p4e8 5968  5p2e7 5969  5p3e8 5970  5p4e9 5971  5p5e10 5972  6p2e8 5973  6p3e9 5974  6p4e10 5975  7p2e9 5976  7p3e10 5977  8p2e10 5978  nnzrab 6114  nn0zrab 6115  seq1suclem 6266  ioomax 6338  ioopos 6339  ioorp 6340  nn0uz 6383  nnuz 6384  seq1seqz 6486  seq0seqz 6487  binom2aOLD 6590  discrlem1 6601  sqrval 6616  sqrlem11 6628  irec 6676  crulem 6681  crmul 6686  cjcj 6728  cjreb 6731  cjmul 6739  addcj 6748  recvalz 6840  facnnt 6885  faclbnd2 6898  faclbnd4lem1 6900  bcpasc2 6920  serzclim0 7062  isumnn0nn 7159  isumclt 7161  geolimilem 7187  geolim1i 7190  0.999... 7198  cncfval 7216  isupivth 7242  ivth2OLD 7251  efclt 7271  efaddlem12 7308  efaddlem20 7316  efaddlem22 7318  eirrlem3 7349  efsep 7354  ef4p 7357  sinadd 7410  cos2tOLD 7423  cos1bnd 7433  cos2bnd 7434  ruclem17 7486  infxpidmlem9 7520  alephsuc3 7545  cnconst 7740  cncfmet1 7868  xplm 7937  opr1scn 7942  ringsn 8127  nvvop 8192  nvvc 8198  vsfval 8218  nvm 8226  cnims 8297  sqcn 8298  ip1cnilem4 8338  ip1cnilem6 8340  ip0i 8443  ip1ilem 8444  ip2i 8446  ipasslem6 8454  ipasslem7 8455  ipasslem10 8458  minveclem27 8530  pilem3 8627  sinhalfpilem 8633  cospi 8636  sincos6thpi 8663  dflog2 8707  h2hva 8798  h2hsm 8799  h2hvs 8801  h2hcau 8804  h2hlm 8805  axhfvadd 8807  axhvcom 8808  axhvass 8809  axhv0cl 8810  axhvaddid 8811  axhfvmul 8812  axhvmulid 8813  axhvmulass 8814  axhvdistr1 8815  axhvdistr2 8816  axhvmul0 8817  axhfi 8818  axhis1 8819  axhis2 8820  axhis3 8821  axhis4 8822  axhcompl 8823  hvsubass 8877  normlem0 8930  normlem1 8931  normlem2 8932  normlem4 8934  normlem9 8939  bcseq 8941  dfhnorm2 8943  normpar 8976  normpar2 8978  polid2 8979  polid 8980  hhba 8989  hhims 8994  hhims2 8995  hhsssh 9094  hhssims 9100  hhssims2 9101  ocvalt 9108  projlem3 9143  pjthlem1 9174  pjthlem5 9178  pjthlem6 9179  spanvalt 9254  hsupval2t 9255  sshjvalt 9275  sshjval3t 9281  shsumval3 9316  hosmvalt 9468  hommvalt 9469  hodmvalt 9470  hfsmvalt 9471  hfmmvalt 9472  cmcm2 9493  fh2t 9519  qlaxr3 9534  pjcj 9586  ho0valt 9633  df0op2 9635  hosd2 9706  eigorth 9720  dfbdop2 9743  hhnmo 9784  hhblo 9785  hh0o 9786  nmop0 9867  nmfn0 9868  lnopeq0lem1 9886  lnophmlem2 9898  nmopcoadj 9990  cvmd 10207  cdj3lem3 10321  cdj3lem3b 10323  ghomgrpilem2 10342  cayleylem2 10366  infi1 10405  cmpbva 10418  hmeogrp 10484  trnij 10553  stoi 10555  jdmo 10627

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468

Copyright terms: Public domain