Theorem eqtr4id 2813

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 2768	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2811	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 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751

This theorem is referenced by:  iftrue  4419  iffalse  4422  difprsn1  4683  dmmptg  6064  setlikespec  6140  funimacnv  6409  dmmptd  6469  resasplit  6526  dffv3  6647  dfimafn  6709  fniinfv  6723  dffv2  6740  fvco2  6742  fniunfv  6991  isoini  7078  fvmpopr2d  7299  zfrep6  7653  oprabco  7789  suppco  7873  oeeulem  8230  ixpconstg  8481  sbthlem4  8644  sbthlem5  8645  sbthlem6  8646  supval2  8937  hartogslem1  9024  cantnflem1d  9169  alephsuc2  9525  dfac3  9566  hsmexlem5  9875  axdc2lem  9893  gruima  10247  eqneg  11383  zeo  12092  fseq1p1m1  13015  hashfzo  13825  hashimarn  13836  wrdval  13901  wrdnval  13929  repswswrd  14178  s1co  14227  swrds2  14334  modfsummod  15182  telfsumo  15190  mulgcd  15932  algcvg  15957  phiprmpw  16153  phisum  16167  strfv3  16575  resslem  16600  pwssnf1o  16814  imassca  16835  homfeq  17007  oppcbas  17031  resscatc  17416  estrcbasbas  17432  funcestrcsetclem7  17447  funcestrcsetclem8  17448  funcestrcsetclem9  17449  fthestrcsetc  17451  fullestrcsetc  17452  equivestrcsetc  17453  setc1strwun  17454  funcsetcestrclem7  17462  funcsetcestrclem8  17463  funcsetcestrclem9  17464  fthsetcestrc  17466  fullsetcestrc  17467  lubsn  17755  ipotset  17818  ipole  17819  plusfeq  17911  pws0g  17998  frmd0  18076  efmndtset  18095  oppgplusfval  18528  gsmsymgrfix  18608  gsmsymgreq  18612  psgnunilem2  18675  sylow3lem2  18805  oppglsm  18819  frgpuplem  18950  frgpupf  18951  frgpup1  18953  frgpup3lem  18955  gsumzoppg  19117  ablfac1eu  19248  pgpfaclem1  19256  pwsmgp  19424  opprmulfval  19431  dfrhm2  19525  subrg1  19598  staffn  19673  issrngd  19685  scafeq  19707  lbsextlem4  19986  sralem  20002  sravsca  20007  sraip  20008  zlmlem  20271  zlmvsca  20276  znbaslem  20291  ipfeq  20400  ssipeq  20406  thlbas  20446  thlle  20447  thloc  20449  dsmmbase  20485  dsmmelbas  20489  frlmelbas  20506  frlmphl  20531  islindf4  20588  rnascl  20639  psrlinv  20710  opsrbaslem  20794  evlseu  20831  mpfsubrg  20851  ply1scl0  20999  evl1sca  21038  evls1var  21042  matbas  21098  matplusg  21099  matsca  21100  matvsca  21101  matbas2d  21108  matsubgcell  21119  matmulcell  21130  ofco2  21136  mattposm  21144  mat1f1o  21163  mdetunilem8  21304  madugsum  21328  cramerimplem2  21369  decpmatmullem  21456  paste  21979  ptpjcn  22296  uptx  22310  xpstopnlem1  22494  alexsubALTlem4  22735  cnextf  22751  submtmd  22789  ussval  22945  tuslem  22953  psmetge0  22999  xmetge0  23031  setsmsds  23163  sgrim  23318  tnglem  23327  tngtset  23336  tngngp2  23339  resubmet  23488  pcorev2  23714  om1plusg  23720  om1tset  23721  om1opn  23722  pi1grplem  23735  clmadd  23760  clmmul  23761  clmcj  23762  tcphtopn  23911  tchnmfval  23913  bcthlem1  24009  bcthlem2  24010  bcthlem4  24012  bcth3  24016  rrxmval  24090  rrxmfval  24091  rrxdsfi  24096  ehlbase  24100  minveclem3b  24113  pjthlem1  24122  volun  24230  voliun  24239  uniioovol  24264  itg2i1fseq  24440  itgcnlem  24474  iblabslem  24512  limcres  24570  cnplimc  24571  ply1termlem  24884  0dgr  24926  taylthlem1  25052  abelth  25120  lawcos  25486  lgambdd  25706  basellem8  25757  musum  25860  chtub  25880  dchrval  25902  dchrinvcl  25921  lgsval4lem  25976  lgsquadlem2  26049  m1lgs  26056  mirauto  26562  lmiisolem  26674  ttglem  26754  axlowdimlem16  26835  ebtwntg  26860  ecgrtg  26861  elntg2  26863  nbgrval  27210  uvtxupgrres  27282  clwlknf1oclwwlknlem3  27952  eucrct2eupth  28114  smcnlem  28564  siii  28720  pjhthlem1  29258  sbcies  30342  imadifxp  30447  dfimafnf  30478  funcnvmpt  30513  symgcom  30863  cycpmconjslem1  30932  rdivmuldivd  30999  resvlem  31041  qusker  31055  idlsrgbas  31155  idlsrgplusg  31156  idlsrgmulr  31158  idlsrgtset  31159  idlsrgmulrval  31160  mdetpmtr12  31281  zarcls  31330  zar0ring  31334  pstmval  31351  xpinpreima2  31363  pnfneige0  31407  zlmds  31418  zlmtset  31419  esumid  31516  esumrnmpt  31524  sxsigon  31664  carsgclctunlem1  31788  circlemethnat  32125  f1resfz0f1d  32574  fnrelpredd  32575  pthhashvtx  32590  filnetlem4  34104  setsstrset  34816  finxpreclem4  35076  itg2addnclem  35373  iblabsnclem  35385  areacirc  35415  fnopabco  35426  heiborlem8  35521  rngoi  35602  drngoi  35654  ldualvsub  36716  dalemrotyz  37219  dalem6  37229  dalem7  37230  dalem11  37235  dalem12  37236  dalemrotps  37252  dalem30  37263  dalem35  37268  cdleme1  37788  cdleme9  37814  cdleme20c  37872  cdleme20d  37873  cdlemefrs29clN  37960  cdleme37m  38023  cdleme43aN  38050  cdlemg1b2  38132  cdlemg4f  38176  cdlemh2  38377  erngdvlem1  38549  erngdvlem2N  38550  erngdvlem3  38551  erngdvlem4  38552  erngdvlem1-rN  38557  erngdvlem2-rN  38558  erngdvlem3-rN  38559  erngdvlem4-rN  38560  dvh4dimN  39008  lcdvsub  39178  hlhilsca  39496  hlhilbase  39497  hlhilplus  39498  hlhilvsca  39508  hlhilip  39509  hlhilipval  39510  rnasclg  39715  evlsval3  39762  evlsbagval  39765  prjspeclsp  39933  mzpcompact2lem  40050  eldioph2lem1  40059  fiphp3d  40118  rmxypairf1o  40210  wopprc  40329  lmhmlnmsplit  40389  clcnvlem  40681  mnringnmulrd  41280  mnringbaserd  41282  mnringmulrd  41289  dmmptdf  42207  dmmptdf2  42222  ellimcabssub0  42610  cosknegpi  42862  fourierdlem58  43157  fourierdlem59  43158  fourierdlem72  43171  fourierdlem80  43179  sqwvfourb  43222  etransclem28  43255  etransclem41  43268  omef  43486  dfaimafn  44074  afv2co2  44166  sbgoldbo  44657  rrxlinesc  45499  rrxlinec  45500  rrx2linest2  45508  rrxsphere  45512  itsclinecirc0b  45538  itsclquadb  45540