Theorem eqtr4id 2789

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 2744	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2787	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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  rabeqcda  3427  iftrue  4506  iffalse  4509  difprsn1  4776  dmmptg  6231  setlikespec  6314  funimacnv  6616  dmmptd  6682  resasplit  6747  dffv3  6871  dfimafn  6940  fniinfv  6956  dffv2  6973  fvco2  6975  fniunfv  7238  isoini  7330  fvmpopr2d  7567  zfrep6  7951  oprabco  8093  suppco  8203  oeeulem  8611  ixpconstg  8918  sbthlem4  9098  sbthlem5  9099  sbthlem6  9100  supval2  9465  hartogslem1  9554  cantnflem1d  9700  alephsuc2  10092  dfac3  10133  hsmexlem5  10442  axdc2lem  10460  gruima  10814  eqneg  11959  zeo  12677  fseq1p1m1  13613  hashfzo  14445  hashimarn  14456  wrdval  14532  wrdnval  14561  repswswrd  14800  s1co  14850  swrds2  14957  s7f1o  14983  modfsummod  15808  telfsumo  15816  mulgcd  16565  algcvg  16593  phiprmpw  16793  phisum  16808  strfv3  17221  resseqnbas  17261  pwssnf1o  17510  imassca  17531  homfeq  17704  oppcbas  17728  resscatc  18120  estrcbasbas  18141  funcestrcsetclem7  18156  funcestrcsetclem8  18157  funcestrcsetclem9  18158  fthestrcsetc  18160  fullestrcsetc  18161  equivestrcsetc  18162  setc1strwun  18163  funcsetcestrclem7  18171  funcsetcestrclem8  18172  funcsetcestrclem9  18173  fthsetcestrc  18175  fullsetcestrc  18176  lubsn  18490  ipotset  18541  ipole  18542  plusfeq  18624  pws0g  18749  frmd0  18836  efmndtset  18855  oppgplusfval  19329  gsmsymgrfix  19407  gsmsymgreq  19411  psgnunilem2  19474  sylow3lem2  19607  oppglsm  19621  frgpuplem  19751  frgpupf  19752  frgpup1  19754  frgpup3lem  19756  gsumzoppg  19923  ablfac1eu  20054  pgpfaclem1  20062  pwsmgp  20285  opprmulfval  20297  rdivmuldivd  20371  dfrhm2  20432  subrg1  20540  staffn  20801  issrngd  20813  scafeq  20837  lbsextlem4  21120  sralem  21132  sravsca  21137  sraip  21138  2idlbas  21222  zlmlem  21475  zlmvsca  21480  znbaslem  21497  ipfeq  21608  ssipeq  21614  thlbas  21654  thlle  21655  thloc  21657  dsmmbase  21693  dsmmelbas  21697  frlmelbas  21714  frlmphl  21739  islindf4  21796  rnascl  21849  psrlinv  21913  opsrbaslem  22005  evlseu  22039  mpfsubrg  22059  psdmvr  22105  ply1scl0OLD  22226  evl1sca  22270  evls1var  22274  matbas  22349  matplusg  22350  matsca  22351  matvsca  22352  matbas2d  22359  matsubgcell  22370  matmulcell  22381  ofco2  22387  mattposm  22395  mat1f1o  22414  mdetunilem8  22555  madugsum  22579  cramerimplem2  22620  decpmatmullem  22707  paste  23230  ptpjcn  23547  uptx  23561  xpstopnlem1  23745  alexsubALTlem4  23986  cnextf  24002  submtmd  24040  ussval  24196  tuslem  24203  psmetge0  24249  xmetge0  24281  setsmsds  24413  sgrim  24568  tnglem  24577  tngtset  24586  tngngp2  24589  resubmet  24739  pcorev2  24977  om1plusg  24983  om1tset  24984  om1opn  24985  pi1grplem  24998  clmadd  25023  clmmul  25024  clmcj  25025  tcphtopn  25176  tchnmfval  25178  bcthlem1  25274  bcthlem2  25275  bcthlem4  25277  bcth3  25281  rrxmval  25355  rrxmfval  25356  rrxdsfi  25361  ehlbase  25365  minveclem3b  25378  pjthlem1  25387  volun  25496  voliun  25505  uniioovol  25530  itg2i1fseq  25706  itgcnlem  25741  iblabslem  25779  limcres  25837  cnplimc  25838  ply1termlem  26158  0dgr  26200  taylthlem1  26331  abelth  26401  lawcos  26776  lgambdd  26997  basellem8  27048  musum  27151  chtub  27173  dchrval  27195  dchrinvcl  27214  lgsval4lem  27269  lgsquadlem2  27342  m1lgs  27349  cuteq0  27794  precsexlem11  28158  seqsval  28211  n0sbday  28271  zseo  28323  mirauto  28609  lmiisolem  28721  ttglem  28801  axlowdimlem16  28882  ebtwntg  28907  ecgrtg  28908  elntg2  28910  nbgrval  29261  uvtxupgrres  29333  clwlknf1oclwwlknlem3  30010  eucrct2eupth  30172  smcnlem  30624  siii  30780  pjhthlem1  31318  sbcies  32415  imadifxp  32528  dfimafnf  32560  funcnvmpt  32591  ccatws1f1olast  32874  gsumwun  33005  symgcom  33040  cycpmconjslem1  33111  rloc0g  33212  rloc1r  33213  resvlem  33295  qusker  33310  elrspunsn  33390  opprqusplusg  33450  idlsrgbas  33465  idlsrgplusg  33466  idlsrgmulr  33468  idlsrgtset  33469  idlsrgmulrval  33470  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  irredminply  33696  algextdeglem4  33700  algextdeglem5  33701  constrrtcc  33715  cos9thpinconstrlem1  33769  mdetpmtr12  33802  zarcls  33851  zar0ring  33855  pstmval  33872  xpinpreima2  33884  pnfneige0  33928  zlmds  33939  zlmtset  33940  esumid  34021  esumrnmpt  34029  sxsigon  34169  carsgclctunlem1  34295  circlemethnat  34619  fnrelpredd  35066  f1resfz0f1d  35082  pthhashvtx  35096  filnetlem4  36345  setsstrset  37100  finxpreclem4  37358  itg2addnclem  37641  iblabsnclem  37653  areacirc  37683  fnopabco  37693  heiborlem8  37788  rngoi  37869  drngoi  37921  ldualvsub  39119  dalemrotyz  39623  dalem6  39633  dalem7  39634  dalem11  39639  dalem12  39640  dalemrotps  39656  dalem30  39667  dalem35  39672  cdleme1  40192  cdleme9  40218  cdleme20c  40276  cdleme20d  40277  cdlemefrs29clN  40364  cdleme37m  40427  cdleme43aN  40454  cdlemg1b2  40536  cdlemg4f  40580  cdlemh2  40781  erngdvlem1  40953  erngdvlem2N  40954  erngdvlem3  40955  erngdvlem4  40956  erngdvlem1-rN  40961  erngdvlem2-rN  40962  erngdvlem3-rN  40963  erngdvlem4-rN  40964  dvh4dimN  41412  lcdvsub  41582  hlhilsca  41900  hlhilbase  41901  hlhilplus  41902  hlhilvsca  41912  hlhilip  41913  hlhilipval  41914  reelznn0nn  42439  rnasclg  42469  evlsval3  42529  prjspeclsp  42582  mzpcompact2lem  42721  eldioph2lem1  42730  fiphp3d  42789  rmxypairf1o  42882  wopprc  43001  lmhmlnmsplit  43058  rp-tfslim  43324  onsucunitp  43344  clcnvlem  43594  mnringnmulrd  44186  mnringbaserd  44188  mnringmulrd  44195  dmmptdff  45195  dmmptdf2  45205  ellimcabssub0  45594  cosknegpi  45846  dvnprodlem1  45923  fourierdlem58  46141  fourierdlem59  46142  fourierdlem72  46155  fourierdlem80  46163  sqwvfourb  46206  etransclem28  46239  etransclem41  46252  omef  46473  dfaimafn  47142  afv2co2  47234  sbgoldbo  47749  rrxlinesc  48663  rrxlinec  48664  rrx2linest2  48672  rrxsphere  48676  itsclinecirc0b  48702  itsclquadb  48704  2oppf  49028  idfullsubc  49048  dfinito4  49334  prstcnid  49378  prstcthin  49386