Theorem eqtr4id 2792

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

Syntax hints:   → wi 4   = wceq 1542

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  rabeqcda  3444  iftrue  4535  iffalse  4538  difprsn1  4804  dmmptg  6242  setlikespec  6327  funimacnv  6630  dmmptd  6696  resasplit  6762  dffv3  6888  dfimafn  6955  fniinfv  6970  dffv2  6987  fvco2  6989  fniunfv  7246  isoini  7335  fvmpopr2d  7569  zfrep6  7941  oprabco  8082  suppco  8191  oeeulem  8601  ixpconstg  8900  sbthlem4  9086  sbthlem5  9087  sbthlem6  9088  supval2  9450  hartogslem1  9537  cantnflem1d  9683  alephsuc2  10075  dfac3  10116  hsmexlem5  10425  axdc2lem  10443  gruima  10797  eqneg  11934  zeo  12648  fseq1p1m1  13575  hashfzo  14389  hashimarn  14400  wrdval  14467  wrdnval  14495  repswswrd  14734  s1co  14784  swrds2  14891  modfsummod  15740  telfsumo  15748  mulgcd  16490  algcvg  16513  phiprmpw  16709  phisum  16723  strfv3  17138  resseqnbas  17186  resslemOLD  17187  pwssnf1o  17444  imassca  17465  homfeq  17638  oppcbas  17663  oppcbasOLD  17664  resscatc  18059  estrcbasbas  18082  funcestrcsetclem7  18098  funcestrcsetclem8  18099  funcestrcsetclem9  18100  fthestrcsetc  18102  fullestrcsetc  18103  equivestrcsetc  18104  setc1strwun  18105  funcsetcestrclem7  18113  funcsetcestrclem8  18114  funcsetcestrclem9  18115  fthsetcestrc  18117  fullsetcestrc  18118  lubsn  18435  ipotset  18486  ipole  18487  plusfeq  18569  pws0g  18661  frmd0  18741  efmndtset  18760  oppgplusfval  19212  gsmsymgrfix  19296  gsmsymgreq  19300  psgnunilem2  19363  sylow3lem2  19496  oppglsm  19510  frgpuplem  19640  frgpupf  19641  frgpup1  19643  frgpup3lem  19645  gsumzoppg  19812  ablfac1eu  19943  pgpfaclem1  19951  pwsmgp  20140  opprmulfval  20152  rdivmuldivd  20227  dfrhm2  20253  subrg1  20329  staffn  20457  issrngd  20469  scafeq  20492  lbsextlem4  20774  sralem  20790  sralemOLD  20791  sravsca  20800  sravscaOLD  20801  sraip  20802  2idlbas  20869  zlmlem  21066  zlmlemOLD  21067  zlmvsca  21075  znbaslem  21090  znbaslemOLD  21091  ipfeq  21203  ssipeq  21209  thlbas  21249  thlbasOLD  21250  thlle  21251  thlleOLD  21252  thloc  21254  dsmmbase  21290  dsmmelbas  21294  frlmelbas  21311  frlmphl  21336  islindf4  21393  rnascl  21445  psrlinv  21516  opsrbaslem  21604  opsrbaslemOLD  21605  evlseu  21646  mpfsubrg  21666  ply1scl0OLD  21813  evl1sca  21853  evls1var  21857  matbas  21913  matplusg  21914  matsca  21915  matscaOLD  21916  matvsca  21917  matvscaOLD  21918  matbas2d  21925  matsubgcell  21936  matmulcell  21947  ofco2  21953  mattposm  21961  mat1f1o  21980  mdetunilem8  22121  madugsum  22145  cramerimplem2  22186  decpmatmullem  22273  paste  22798  ptpjcn  23115  uptx  23129  xpstopnlem1  23313  alexsubALTlem4  23554  cnextf  23570  submtmd  23608  ussval  23764  tuslem  23771  tuslemOLD  23772  psmetge0  23818  xmetge0  23850  setsmsds  23983  setsmsdsOLD  23984  sgrim  24140  tnglem  24149  tnglemOLD  24150  tngtset  24166  tngngp2  24169  resubmet  24318  pcorev2  24544  om1plusg  24550  om1tset  24551  om1opn  24552  pi1grplem  24565  clmadd  24590  clmmul  24591  clmcj  24592  tcphtopn  24743  tchnmfval  24745  bcthlem1  24841  bcthlem2  24842  bcthlem4  24844  bcth3  24848  rrxmval  24922  rrxmfval  24923  rrxdsfi  24928  ehlbase  24932  minveclem3b  24945  pjthlem1  24954  volun  25062  voliun  25071  uniioovol  25096  itg2i1fseq  25273  itgcnlem  25307  iblabslem  25345  limcres  25403  cnplimc  25404  ply1termlem  25717  0dgr  25759  taylthlem1  25885  abelth  25953  lawcos  26321  lgambdd  26541  basellem8  26592  musum  26695  chtub  26715  dchrval  26737  dchrinvcl  26756  lgsval4lem  26811  lgsquadlem2  26884  m1lgs  26891  cuteq0  27333  precsexlem11  27663  mirauto  27935  lmiisolem  28047  ttglem  28128  ttglemOLD  28129  axlowdimlem16  28215  ebtwntg  28240  ecgrtg  28241  elntg2  28243  nbgrval  28593  uvtxupgrres  28665  clwlknf1oclwwlknlem3  29336  eucrct2eupth  29498  smcnlem  29950  siii  30106  pjhthlem1  30644  sbcies  31728  imadifxp  31832  dfimafnf  31860  funcnvmpt  31892  symgcom  32244  cycpmconjslem1  32313  resvlem  32445  resvlemOLD  32446  qusker  32464  elrspunsn  32547  opprqusplusg  32603  idlsrgbas  32618  idlsrgplusg  32619  idlsrgmulr  32621  idlsrgtset  32622  idlsrgmulrval  32623  algextdeglem1  32772  mdetpmtr12  32805  zarcls  32854  zar0ring  32858  pstmval  32875  xpinpreima2  32887  pnfneige0  32931  zlmds  32942  zlmdsOLD  32943  zlmtset  32944  zlmtsetOLD  32945  esumid  33042  esumrnmpt  33050  sxsigon  33190  carsgclctunlem1  33316  circlemethnat  33653  fnrelpredd  34092  f1resfz0f1d  34103  pthhashvtx  34118  filnetlem4  35266  setsstrset  36017  finxpreclem4  36275  itg2addnclem  36539  iblabsnclem  36551  areacirc  36581  fnopabco  36591  heiborlem8  36686  rngoi  36767  drngoi  36819  ldualvsub  38025  dalemrotyz  38529  dalem6  38539  dalem7  38540  dalem11  38545  dalem12  38546  dalemrotps  38562  dalem30  38573  dalem35  38578  cdleme1  39098  cdleme9  39124  cdleme20c  39182  cdleme20d  39183  cdlemefrs29clN  39270  cdleme37m  39333  cdleme43aN  39360  cdlemg1b2  39442  cdlemg4f  39486  cdlemh2  39687  erngdvlem1  39859  erngdvlem2N  39860  erngdvlem3  39861  erngdvlem4  39862  erngdvlem1-rN  39867  erngdvlem2-rN  39868  erngdvlem3-rN  39869  erngdvlem4-rN  39870  dvh4dimN  40318  lcdvsub  40488  hlhilsca  40806  hlhilbase  40807  hlhilplus  40808  hlhilvsca  40822  hlhilip  40823  hlhilipval  40824  rnasclg  41073  evlsval3  41131  reelznn0nn  41322  prjspeclsp  41354  mzpcompact2lem  41489  eldioph2lem1  41498  fiphp3d  41557  rmxypairf1o  41650  wopprc  41769  lmhmlnmsplit  41829  rp-tfslim  42103  onsucunitp  42123  clcnvlem  42374  mnringnmulrd  42968  mnringnmulrdOLD  42969  mnringbaserd  42972  mnringmulrd  42980  dmmptdff  43922  dmmptdf2  43935  ellimcabssub0  44333  cosknegpi  44585  fourierdlem58  44880  fourierdlem59  44881  fourierdlem72  44894  fourierdlem80  44902  sqwvfourb  44945  etransclem28  44978  etransclem41  44991  omef  45212  dfaimafn  45873  afv2co2  45965  sbgoldbo  46455  rrxlinesc  47421  rrxlinec  47422  rrx2linest2  47430  rrxsphere  47434  itsclinecirc0b  47460  itsclquadb  47462  prstcnid  47686  prstcthin  47696