Theorem eqtr4id 2798

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr4id.2	⊢ 𝐴 = 𝐵
eqtr4id.1	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4id

Step	Hyp	Ref	Expression
1		eqtr4id.1	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
2		eqtr4id.2	. . 3 ⊢ 𝐴 = 𝐵
3	2	eqcomi 2748	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2796	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  iftrue  4466  iffalse  4469  difprsn1  4734  dmmptg  6150  setlikespec  6232  funimacnv  6522  dmmptd  6587  resasplit  6653  dffv3  6779  dfimafn  6841  fniinfv  6855  dffv2  6872  fvco2  6874  fniunfv  7129  isoini  7218  fvmpopr2d  7443  zfrep6  7806  oprabco  7945  suppco  8031  oeeulem  8441  ixpconstg  8703  sbthlem4  8882  sbthlem5  8883  sbthlem6  8884  supval2  9223  hartogslem1  9310  cantnflem1d  9455  alephsuc2  9845  dfac3  9886  hsmexlem5  10195  axdc2lem  10213  gruima  10567  eqneg  11704  zeo  12415  fseq1p1m1  13339  hashfzo  14153  hashimarn  14164  wrdval  14229  wrdnval  14257  repswswrd  14506  s1co  14555  swrds2  14662  modfsummod  15515  telfsumo  15523  mulgcd  16265  algcvg  16290  phiprmpw  16486  phisum  16500  strfv3  16915  resseqnbas  16960  resslemOLD  16961  pwssnf1o  17218  imassca  17239  homfeq  17412  oppcbas  17437  oppcbasOLD  17438  resscatc  17833  estrcbasbas  17856  funcestrcsetclem7  17872  funcestrcsetclem8  17873  funcestrcsetclem9  17874  fthestrcsetc  17876  fullestrcsetc  17877  equivestrcsetc  17878  setc1strwun  17879  funcsetcestrclem7  17887  funcsetcestrclem8  17888  funcsetcestrclem9  17889  fthsetcestrc  17891  fullsetcestrc  17892  lubsn  18209  ipotset  18260  ipole  18261  plusfeq  18343  pws0g  18430  frmd0  18508  efmndtset  18527  oppgplusfval  18961  gsmsymgrfix  19045  gsmsymgreq  19049  psgnunilem2  19112  sylow3lem2  19242  oppglsm  19256  frgpuplem  19387  frgpupf  19388  frgpup1  19390  frgpup3lem  19392  gsumzoppg  19554  ablfac1eu  19685  pgpfaclem1  19693  pwsmgp  19866  opprmulfval  19873  dfrhm2  19970  subrg1  20043  staffn  20118  issrngd  20130  scafeq  20152  lbsextlem4  20432  sralem  20448  sralemOLD  20449  sravsca  20458  sravscaOLD  20459  sraip  20460  zlmlem  20727  zlmlemOLD  20728  zlmvsca  20736  znbaslem  20751  znbaslemOLD  20752  ipfeq  20864  ssipeq  20870  thlbas  20910  thlbasOLD  20911  thlle  20912  thlleOLD  20913  thloc  20915  dsmmbase  20951  dsmmelbas  20955  frlmelbas  20972  frlmphl  20997  islindf4  21054  rnascl  21104  psrlinv  21175  opsrbaslem  21259  opsrbaslemOLD  21260  evlseu  21302  mpfsubrg  21322  ply1scl0  21470  evl1sca  21509  evls1var  21513  matbas  21569  matplusg  21570  matsca  21571  matscaOLD  21572  matvsca  21573  matvscaOLD  21574  matbas2d  21581  matsubgcell  21592  matmulcell  21603  ofco2  21609  mattposm  21617  mat1f1o  21636  mdetunilem8  21777  madugsum  21801  cramerimplem2  21842  decpmatmullem  21929  paste  22454  ptpjcn  22771  uptx  22785  xpstopnlem1  22969  alexsubALTlem4  23210  cnextf  23226  submtmd  23264  ussval  23420  tuslem  23427  tuslemOLD  23428  psmetge0  23474  xmetge0  23506  setsmsds  23639  setsmsdsOLD  23640  sgrim  23796  tnglem  23805  tnglemOLD  23806  tngtset  23822  tngngp2  23825  resubmet  23974  pcorev2  24200  om1plusg  24206  om1tset  24207  om1opn  24208  pi1grplem  24221  clmadd  24246  clmmul  24247  clmcj  24248  tcphtopn  24399  tchnmfval  24401  bcthlem1  24497  bcthlem2  24498  bcthlem4  24500  bcth3  24504  rrxmval  24578  rrxmfval  24579  rrxdsfi  24584  ehlbase  24588  minveclem3b  24601  pjthlem1  24610  volun  24718  voliun  24727  uniioovol  24752  itg2i1fseq  24929  itgcnlem  24963  iblabslem  25001  limcres  25059  cnplimc  25060  ply1termlem  25373  0dgr  25415  taylthlem1  25541  abelth  25609  lawcos  25975  lgambdd  26195  basellem8  26246  musum  26349  chtub  26369  dchrval  26391  dchrinvcl  26410  lgsval4lem  26465  lgsquadlem2  26538  m1lgs  26545  mirauto  27054  lmiisolem  27166  ttglem  27247  ttglemOLD  27248  axlowdimlem16  27334  ebtwntg  27359  ecgrtg  27360  elntg2  27362  nbgrval  27712  uvtxupgrres  27784  clwlknf1oclwwlknlem3  28456  eucrct2eupth  28618  smcnlem  29068  siii  29224  pjhthlem1  29762  sbcies  30845  imadifxp  30949  dfimafnf  30980  funcnvmpt  31013  symgcom  31361  cycpmconjslem1  31430  rdivmuldivd  31497  resvlem  31539  resvlemOLD  31540  qusker  31558  idlsrgbas  31658  idlsrgplusg  31659  idlsrgmulr  31661  idlsrgtset  31662  idlsrgmulrval  31663  mdetpmtr12  31784  zarcls  31833  zar0ring  31837  pstmval  31854  xpinpreima2  31866  pnfneige0  31910  zlmds  31921  zlmdsOLD  31922  zlmtset  31923  zlmtsetOLD  31924  esumid  32021  esumrnmpt  32029  sxsigon  32169  carsgclctunlem1  32293  circlemethnat  32630  fnrelpredd  33070  f1resfz0f1d  33081  pthhashvtx  33098  filnetlem4  34579  setsstrset  35316  finxpreclem4  35574  itg2addnclem  35837  iblabsnclem  35849  areacirc  35879  fnopabco  35890  heiborlem8  35985  rngoi  36066  drngoi  36118  ldualvsub  37176  dalemrotyz  37679  dalem6  37689  dalem7  37690  dalem11  37695  dalem12  37696  dalemrotps  37712  dalem30  37723  dalem35  37728  cdleme1  38248  cdleme9  38274  cdleme20c  38332  cdleme20d  38333  cdlemefrs29clN  38420  cdleme37m  38483  cdleme43aN  38510  cdlemg1b2  38592  cdlemg4f  38636  cdlemh2  38837  erngdvlem1  39009  erngdvlem2N  39010  erngdvlem3  39011  erngdvlem4  39012  erngdvlem1-rN  39017  erngdvlem2-rN  39018  erngdvlem3-rN  39019  erngdvlem4-rN  39020  dvh4dimN  39468  lcdvsub  39638  hlhilsca  39956  hlhilbase  39957  hlhilplus  39958  hlhilvsca  39972  hlhilip  39973  hlhilipval  39974  rnasclg  40230  evlsval3  40279  evlsbagval  40282  prjspeclsp  40458  mzpcompact2lem  40580  eldioph2lem1  40589  fiphp3d  40648  rmxypairf1o  40740  wopprc  40859  lmhmlnmsplit  40919  clcnvlem  41238  mnringnmulrd  41834  mnringnmulrdOLD  41835  mnringbaserd  41838  mnringmulrd  41846  dmmptdf  42770  dmmptdf2  42783  ellimcabssub0  43165  cosknegpi  43417  fourierdlem58  43712  fourierdlem59  43713  fourierdlem72  43726  fourierdlem80  43734  sqwvfourb  43777  etransclem28  43810  etransclem41  43823  omef  44041  dfaimafn  44668  afv2co2  44760  sbgoldbo  45250  rrxlinesc  46092  rrxlinec  46093  rrx2linest2  46101  rrxsphere  46105  itsclinecirc0b  46131  itsclquadb  46133  prstcnid  46358  prstcthin  46368