Theorem eqtr4id 2783

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 2738	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2781	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  rabeqcda  3417  iftrue  4494  iffalse  4497  difprsn1  4764  dmmptg  6215  setlikespec  6298  funimacnv  6597  dmmptd  6663  resasplit  6730  dffv3  6854  dfimafn  6923  fniinfv  6939  dffv2  6956  fvco2  6958  fniunfv  7221  isoini  7313  fvmpopr2d  7551  zfrep6  7933  oprabco  8075  suppco  8185  oeeulem  8565  ixpconstg  8879  sbthlem4  9054  sbthlem5  9055  sbthlem6  9056  supval2  9406  hartogslem1  9495  cantnflem1d  9641  alephsuc2  10033  dfac3  10074  hsmexlem5  10383  axdc2lem  10401  gruima  10755  eqneg  11902  zeo  12620  fseq1p1m1  13559  hashfzo  14394  hashimarn  14405  wrdval  14481  wrdnval  14510  repswswrd  14749  s1co  14799  swrds2  14906  s7f1o  14932  modfsummod  15760  telfsumo  15768  mulgcd  16518  algcvg  16546  phiprmpw  16746  phisum  16761  strfv3  17174  resseqnbas  17212  pwssnf1o  17461  imassca  17482  homfeq  17655  oppcbas  17679  resscatc  18071  estrcbasbas  18092  funcestrcsetclem7  18107  funcestrcsetclem8  18108  funcestrcsetclem9  18109  fthestrcsetc  18111  fullestrcsetc  18112  equivestrcsetc  18113  setc1strwun  18114  funcsetcestrclem7  18122  funcsetcestrclem8  18123  funcsetcestrclem9  18124  fthsetcestrc  18126  fullsetcestrc  18127  lubsn  18441  ipotset  18492  ipole  18493  plusfeq  18575  pws0g  18700  frmd0  18787  efmndtset  18806  oppgplusfval  19280  gsmsymgrfix  19358  gsmsymgreq  19362  psgnunilem2  19425  sylow3lem2  19558  oppglsm  19572  frgpuplem  19702  frgpupf  19703  frgpup1  19705  frgpup3lem  19707  gsumzoppg  19874  ablfac1eu  20005  pgpfaclem1  20013  pwsmgp  20236  opprmulfval  20248  rdivmuldivd  20322  dfrhm2  20383  subrg1  20491  staffn  20752  issrngd  20764  scafeq  20788  lbsextlem4  21071  sralem  21083  sravsca  21088  sraip  21089  2idlbas  21173  zlmlem  21426  zlmvsca  21431  znbaslem  21448  ipfeq  21559  ssipeq  21565  thlbas  21605  thlle  21606  thloc  21608  dsmmbase  21644  dsmmelbas  21648  frlmelbas  21665  frlmphl  21690  islindf4  21747  rnascl  21800  psrlinv  21864  opsrbaslem  21956  evlseu  21990  mpfsubrg  22010  psdmvr  22056  ply1scl0OLD  22177  evl1sca  22221  evls1var  22225  matbas  22300  matplusg  22301  matsca  22302  matvsca  22303  matbas2d  22310  matsubgcell  22321  matmulcell  22332  ofco2  22338  mattposm  22346  mat1f1o  22365  mdetunilem8  22506  madugsum  22530  cramerimplem2  22571  decpmatmullem  22658  paste  23181  ptpjcn  23498  uptx  23512  xpstopnlem1  23696  alexsubALTlem4  23937  cnextf  23953  submtmd  23991  ussval  24147  tuslem  24154  psmetge0  24200  xmetge0  24232  setsmsds  24364  sgrim  24519  tnglem  24528  tngtset  24537  tngngp2  24540  resubmet  24690  pcorev2  24928  om1plusg  24934  om1tset  24935  om1opn  24936  pi1grplem  24949  clmadd  24974  clmmul  24975  clmcj  24976  tcphtopn  25126  tchnmfval  25128  bcthlem1  25224  bcthlem2  25225  bcthlem4  25227  bcth3  25231  rrxmval  25305  rrxmfval  25306  rrxdsfi  25311  ehlbase  25315  minveclem3b  25328  pjthlem1  25337  volun  25446  voliun  25455  uniioovol  25480  itg2i1fseq  25656  itgcnlem  25691  iblabslem  25729  limcres  25787  cnplimc  25788  ply1termlem  26108  0dgr  26150  taylthlem1  26281  abelth  26351  lawcos  26726  lgambdd  26947  basellem8  26998  musum  27101  chtub  27123  dchrval  27145  dchrinvcl  27164  lgsval4lem  27219  lgsquadlem2  27292  m1lgs  27299  cuteq0  27744  precsexlem11  28119  seqsval  28182  n0sbday  28244  zseo  28308  mirauto  28611  lmiisolem  28723  ttglem  28803  axlowdimlem16  28884  ebtwntg  28909  ecgrtg  28910  elntg2  28912  nbgrval  29263  uvtxupgrres  29335  clwlknf1oclwwlknlem3  30012  eucrct2eupth  30174  smcnlem  30626  siii  30782  pjhthlem1  31320  sbcies  32417  imadifxp  32530  dfimafnf  32560  funcnvmpt  32591  ccatws1f1olast  32874  gsumwun  33005  symgcom  33040  cycpmconjslem1  33111  rloc0g  33222  rloc1r  33223  resvlem  33305  qusker  33320  elrspunsn  33400  opprqusplusg  33460  idlsrgbas  33475  idlsrgplusg  33476  idlsrgmulr  33478  idlsrgtset  33479  idlsrgmulrval  33480  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  irredminply  33706  algextdeglem4  33710  algextdeglem5  33711  constrrtcc  33725  cos9thpinconstrlem1  33779  mdetpmtr12  33815  zarcls  33864  zar0ring  33868  pstmval  33885  xpinpreima2  33897  pnfneige0  33941  zlmds  33952  zlmtset  33953  esumid  34034  esumrnmpt  34042  sxsigon  34182  carsgclctunlem1  34308  circlemethnat  34632  fnrelpredd  35079  f1resfz0f1d  35101  pthhashvtx  35115  filnetlem4  36369  setsstrset  37124  finxpreclem4  37382  itg2addnclem  37665  iblabsnclem  37677  areacirc  37707  fnopabco  37717  heiborlem8  37812  rngoi  37893  drngoi  37945  ldualvsub  39148  dalemrotyz  39652  dalem6  39662  dalem7  39663  dalem11  39668  dalem12  39669  dalemrotps  39685  dalem30  39696  dalem35  39701  cdleme1  40221  cdleme9  40247  cdleme20c  40305  cdleme20d  40306  cdlemefrs29clN  40393  cdleme37m  40456  cdleme43aN  40483  cdlemg1b2  40565  cdlemg4f  40609  cdlemh2  40810  erngdvlem1  40982  erngdvlem2N  40983  erngdvlem3  40984  erngdvlem4  40985  erngdvlem1-rN  40990  erngdvlem2-rN  40991  erngdvlem3-rN  40992  erngdvlem4-rN  40993  dvh4dimN  41441  lcdvsub  41611  hlhilsca  41929  hlhilbase  41930  hlhilplus  41931  hlhilvsca  41941  hlhilip  41942  hlhilipval  41943  reelznn0nn  42449  rnasclg  42487  evlsval3  42547  prjspeclsp  42600  mzpcompact2lem  42739  eldioph2lem1  42748  fiphp3d  42807  rmxypairf1o  42900  wopprc  43019  lmhmlnmsplit  43076  rp-tfslim  43342  onsucunitp  43362  clcnvlem  43612  mnringnmulrd  44203  mnringbaserd  44205  mnringmulrd  44212  dmmptdff  45217  dmmptdf2  45227  ellimcabssub0  45615  cosknegpi  45867  dvnprodlem1  45944  fourierdlem58  46162  fourierdlem59  46163  fourierdlem72  46176  fourierdlem80  46184  sqwvfourb  46227  etransclem28  46260  etransclem41  46273  omef  46494  dfaimafn  47166  afv2co2  47258  sbgoldbo  47788  rrxlinesc  48724  rrxlinec  48725  rrx2linest2  48733  rrxsphere  48737  itsclinecirc0b  48763  itsclquadb  48765  2oppf  49121  idfullsubc  49150  oppc1stf  49277  oppc2ndf  49278  dfinito4  49490  prstcnid  49542  prstcthin  49550