Theorem eqtr4id 2816

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  rabeqcda  3426  iftrue  4492  iffalse  4495  difprsn1  4767  csbcnv  5871  dmmptg  6242  setlikespec  6326  funimacnv  6617  dmmptd  6680  resasplit  6748  dffv3  6877  dfimafn  6943  fniinfv  6959  dffv2  6976  fvco2  6978  funcnvmpt  6991  fniunfv  7245  isoini  7336  fvmpopr2d  7574  zfrep6OLD  7950  oprabco  8089  suppco  8200  oeeulem  8585  ixpconstg  8902  sbthlem4  9076  sbthlem5  9077  sbthlem6  9078  supval2  9413  hartogslem1  9502  cantnflem1d  9655  alephsuc2  10071  dfac3  10112  hsmexlem5  10420  axdc2lem  10438  gruima  10793  eqneg  11941  zeo  12688  fseq1p1m1  13633  hashfzo  14473  hashimarn  14484  wrdval  14560  wrdnval  14589  repswswrd  14828  s1co  14877  swrds2  14984  s7f1o  15010  modfsummod  15853  telfsumo  15861  indsumhash  15888  mulgcd  16612  algcvg  16640  phiprmpw  16841  phisum  16856  strfv3  17270  resseqnbas  17308  pwssnf1o  17558  imassca  17579  homfeq  17756  oppcbas  17780  resscatc  18172  estrcbasbas  18193  funcestrcsetclem7  18208  funcestrcsetclem8  18209  funcestrcsetclem9  18210  fthestrcsetc  18212  fullestrcsetc  18213  equivestrcsetc  18214  setc1strwun  18215  funcsetcestrclem7  18223  funcsetcestrclem8  18224  funcsetcestrclem9  18225  fthsetcestrc  18227  fullsetcestrc  18228  lubsn  18544  ipotset  18595  ipole  18596  plusfeq  18712  pws0g  18837  frmd0  18925  efmndtset  18944  oppgplusfval  19424  gsmsymgrfix  19504  gsmsymgreq  19508  psgnunilem2  19571  sylow3lem2  19704  oppglsm  19718  frgpuplem  19848  frgpupf  19849  frgpup1  19851  frgpup3lem  19853  gsumzoppg  20020  ablfac1eu  20151  pgpfaclem1  20159  pwsmgp  20415  opprmulfval  20428  rdivmuldivd  20502  dfrhm2  20563  subrg1  20692  staffn  20957  issrngd  20969  scafeq  21014  lbsextlem4  21296  sralem  21308  sravsca  21313  sraip  21314  2idlbas  21413  zlmlem  21677  zlmvsca  21682  znbaslem  21699  ipfeq  21811  ssipeq  21817  thlbas  21857  thlle  21858  thloc  21860  dsmmbase  21896  dsmmelbas  21900  frlmelbas  21917  frlmphl  21942  islindf4  21999  rnascl  22052  psrlinv  22116  opsrbaslem  22211  evlseu  22245  evlsval3  22251  mpfsubrg  22273  psdmvr  22343  evl1sca  22505  evls1var  22509  matbas  22581  matplusg  22582  matsca  22583  matvsca  22584  matbas2d  22591  matsubgcell  22602  matmulcell  22613  ofco2  22619  mattposm  22627  mat1f1o  22646  mdetunilem8  22787  madugsum  22811  cramerimplem2  22852  decpmatmullem  22939  paste  23462  ptpjcn  23779  uptx  23793  xpstopnlem1  23977  alexsubALTlem4  24218  cnextf  24234  submtmd  24272  ussval  24427  tuslem  24434  psmetge0  24480  xmetge0  24512  setsmsds  24644  sgrim  24799  tnglem  24808  tngtset  24817  tngngp2  24820  resubmet  24970  pcorev2  25198  om1plusg  25204  om1tset  25205  om1opn  25206  pi1grplem  25219  clmadd  25244  clmmul  25245  clmcj  25246  tcphtopn  25396  tchnmfval  25398  bcthlem1  25494  bcthlem2  25495  bcthlem4  25497  bcth3  25501  rrxmval  25575  rrxmfval  25576  rrxdsfi  25581  ehlbase  25585  minveclem3b  25598  pjthlem1  25607  volun  25715  voliun  25724  uniioovol  25749  itg2i1fseq  25925  itgcnlem  25960  iblabslem  25998  limcres  26056  cnplimc  26057  ply1termlem  26371  0dgr  26413  taylthlem1  26547  abelth  26615  lawcos  26992  lgambdd  27212  basellem8  27263  musum  27366  chtub  27387  dchrval  27409  dchrinvcl  27428  lgsval4lem  27483  lgsquadlem2  27556  m1lgs  27563  cuteq0  28019  precsexlem11  28421  seqsval  28492  n0bday  28556  zseo  28626  mirauto  28972  lmiisolem  29116  ttglem  29236  axlowdimlem16  29318  ebtwntg  29343  ecgrtg  29344  elntg2  29346  nbgrval  29697  uvtxupgrres  29769  clwlknf1oclwwlknlem3  30445  eucrct2eupth  30607  smcnlem  31060  siii  31216  pjhthlem1  31754  sbcies  32845  imadifxp  32957  dfimafnf  32992  ccatws1f1olast  33281  gsummulsubdishift1  33397  gsumwun  33405  symgcom  33412  cycpmconjslem1  33483  rloc0g  33601  rloc1r  33602  resvlem  33662  qusker  33678  elrspunsn  33746  opprqusplusg  33780  idlsrgbas  33803  idlsrgplusg  33804  idlsrgmulr  33806  idlsrgtset  33807  idlsrgmulrval  33808  fldextrspundgdvdslem  34079  fldextrspundgdvds  34080  irredminply  34115  algextdeglem4  34119  algextdeglem5  34120  constrrtcc  34134  cos9thpinconstrlem1  34188  mdetpmtr12  34224  zarcls  34273  zar0ring  34277  pstmval  34294  xpinpreima2  34306  pnfneige0  34350  zlmds  34361  zlmtset  34362  esumid  34443  esumrnmpt  34451  sxsigon  34591  carsgclctunlem1  34716  circlemethnat  35037  fnrelpredd  35491  f1resfz0f1d  35613  pthhashvtx  35628  filnetlem4  36920  setsstrset  37806  finxpreclem4  38068  itg2addnclem  38350  iblabsnclem  38362  areacirc  38392  fnopabco  38402  heiborlem8  38497  rngoi  38578  drngoi  38630  ldualvsub  39957  dalemrotyz  40460  dalem6  40470  dalem7  40471  dalem11  40476  dalem12  40477  dalemrotps  40493  dalem30  40504  dalem35  40509  cdleme1  41029  cdleme9  41055  cdleme20c  41113  cdleme20d  41114  cdlemefrs29clN  41201  cdleme37m  41264  cdleme43aN  41291  cdlemg1b2  41373  cdlemg4f  41417  cdlemh2  41618  erngdvlem1  41790  erngdvlem2N  41791  erngdvlem3  41792  erngdvlem4  41793  erngdvlem1-rN  41798  erngdvlem2-rN  41799  erngdvlem3-rN  41800  erngdvlem4-rN  41801  dvh4dimN  42249  lcdvsub  42419  hlhilsca  42737  hlhilbase  42738  hlhilplus  42739  hlhilvsca  42749  hlhilip  42750  hlhilipval  42751  25or6to4  43001  reelznn0nn  43263  rnasclg  43301  prjspeclsp  43372  mzpcompact2lem  43510  eldioph2lem1  43519  fiphp3d  43574  rmxypairf1o  43666  wopprc  43785  lmhmlnmsplit  43842  rp-tfslim  44108  onsucunitp  44128  clcnvlem  44377  mnringnmulrd  44966  mnringbaserd  44968  mnringmulrd  44975  dmmptdff  45967  dmmptdf2  45976  ellimcabssub0  46361  cosknegpi  46611  dvnprodlem1  46688  fourierdlem58  46906  fourierdlem59  46907  fourierdlem72  46920  fourierdlem80  46928  sqwvfourb  46971  etransclem28  47004  etransclem41  47017  omef  47238  dfaimafn  47930  afv2co2  48022  sbgoldbo  48580  rrxlinesc  49543  rrxlinec  49544  rrx2linest2  49552  rrxsphere  49556  itsclinecirc0b  49582  itsclquadb  49584  2oppf  49938  idfullsubc  49967  oppc1stf  50094  oppc2ndf  50095  dfinito4  50307  prstcnid  50359  prstcthin  50367