Theorem eqtr4id 2791

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  rabeqcda  3443  iftrue  4533  iffalse  4536  difprsn1  4802  dmmptg  6238  setlikespec  6323  funimacnv  6626  dmmptd  6692  resasplit  6758  dffv3  6884  dfimafn  6951  fniinfv  6966  dffv2  6983  fvco2  6985  fniunfv  7242  isoini  7331  fvmpopr2d  7565  zfrep6  7937  oprabco  8078  suppco  8187  oeeulem  8597  ixpconstg  8896  sbthlem4  9082  sbthlem5  9083  sbthlem6  9084  supval2  9446  hartogslem1  9533  cantnflem1d  9679  alephsuc2  10071  dfac3  10112  hsmexlem5  10421  axdc2lem  10439  gruima  10793  eqneg  11930  zeo  12644  fseq1p1m1  13571  hashfzo  14385  hashimarn  14396  wrdval  14463  wrdnval  14491  repswswrd  14730  s1co  14780  swrds2  14887  modfsummod  15736  telfsumo  15744  mulgcd  16486  algcvg  16509  phiprmpw  16705  phisum  16719  strfv3  17134  resseqnbas  17182  resslemOLD  17183  pwssnf1o  17440  imassca  17461  homfeq  17634  oppcbas  17659  oppcbasOLD  17660  resscatc  18055  estrcbasbas  18078  funcestrcsetclem7  18094  funcestrcsetclem8  18095  funcestrcsetclem9  18096  fthestrcsetc  18098  fullestrcsetc  18099  equivestrcsetc  18100  setc1strwun  18101  funcsetcestrclem7  18109  funcsetcestrclem8  18110  funcsetcestrclem9  18111  fthsetcestrc  18113  fullsetcestrc  18114  lubsn  18431  ipotset  18482  ipole  18483  plusfeq  18565  pws0g  18657  frmd0  18737  efmndtset  18756  oppgplusfval  19206  gsmsymgrfix  19290  gsmsymgreq  19294  psgnunilem2  19357  sylow3lem2  19490  oppglsm  19504  frgpuplem  19634  frgpupf  19635  frgpup1  19637  frgpup3lem  19639  gsumzoppg  19806  ablfac1eu  19937  pgpfaclem1  19945  pwsmgp  20133  opprmulfval  20144  rdivmuldivd  20219  dfrhm2  20245  subrg1  20365  staffn  20449  issrngd  20461  scafeq  20484  lbsextlem4  20766  sralem  20782  sralemOLD  20783  sravsca  20792  sravscaOLD  20793  sraip  20794  2idlbas  20861  zlmlem  21057  zlmlemOLD  21058  zlmvsca  21066  znbaslem  21081  znbaslemOLD  21082  ipfeq  21194  ssipeq  21200  thlbas  21240  thlbasOLD  21241  thlle  21242  thlleOLD  21243  thloc  21245  dsmmbase  21281  dsmmelbas  21285  frlmelbas  21302  frlmphl  21327  islindf4  21384  rnascl  21436  psrlinv  21507  opsrbaslem  21595  opsrbaslemOLD  21596  evlseu  21637  mpfsubrg  21657  ply1scl0OLD  21804  evl1sca  21844  evls1var  21848  matbas  21904  matplusg  21905  matsca  21906  matscaOLD  21907  matvsca  21908  matvscaOLD  21909  matbas2d  21916  matsubgcell  21927  matmulcell  21938  ofco2  21944  mattposm  21952  mat1f1o  21971  mdetunilem8  22112  madugsum  22136  cramerimplem2  22177  decpmatmullem  22264  paste  22789  ptpjcn  23106  uptx  23120  xpstopnlem1  23304  alexsubALTlem4  23545  cnextf  23561  submtmd  23599  ussval  23755  tuslem  23762  tuslemOLD  23763  psmetge0  23809  xmetge0  23841  setsmsds  23974  setsmsdsOLD  23975  sgrim  24131  tnglem  24140  tnglemOLD  24141  tngtset  24157  tngngp2  24160  resubmet  24309  pcorev2  24535  om1plusg  24541  om1tset  24542  om1opn  24543  pi1grplem  24556  clmadd  24581  clmmul  24582  clmcj  24583  tcphtopn  24734  tchnmfval  24736  bcthlem1  24832  bcthlem2  24833  bcthlem4  24835  bcth3  24839  rrxmval  24913  rrxmfval  24914  rrxdsfi  24919  ehlbase  24923  minveclem3b  24936  pjthlem1  24945  volun  25053  voliun  25062  uniioovol  25087  itg2i1fseq  25264  itgcnlem  25298  iblabslem  25336  limcres  25394  cnplimc  25395  ply1termlem  25708  0dgr  25750  taylthlem1  25876  abelth  25944  lawcos  26310  lgambdd  26530  basellem8  26581  musum  26684  chtub  26704  dchrval  26726  dchrinvcl  26745  lgsval4lem  26800  lgsquadlem2  26873  m1lgs  26880  cuteq0  27322  precsexlem11  27652  mirauto  27924  lmiisolem  28036  ttglem  28117  ttglemOLD  28118  axlowdimlem16  28204  ebtwntg  28229  ecgrtg  28230  elntg2  28232  nbgrval  28582  uvtxupgrres  28654  clwlknf1oclwwlknlem3  29325  eucrct2eupth  29487  smcnlem  29937  siii  30093  pjhthlem1  30631  sbcies  31715  imadifxp  31819  dfimafnf  31847  funcnvmpt  31879  symgcom  32231  cycpmconjslem1  32300  resvlem  32433  resvlemOLD  32434  qusker  32452  elrspunsn  32535  opprqusplusg  32591  idlsrgbas  32606  idlsrgplusg  32607  idlsrgmulr  32609  idlsrgtset  32610  idlsrgmulrval  32611  algextdeglem1  32760  mdetpmtr12  32793  zarcls  32842  zar0ring  32846  pstmval  32863  xpinpreima2  32875  pnfneige0  32919  zlmds  32930  zlmdsOLD  32931  zlmtset  32932  zlmtsetOLD  32933  esumid  33030  esumrnmpt  33038  sxsigon  33178  carsgclctunlem1  33304  circlemethnat  33641  fnrelpredd  34080  f1resfz0f1d  34091  pthhashvtx  34106  filnetlem4  35254  setsstrset  36005  finxpreclem4  36263  itg2addnclem  36527  iblabsnclem  36539  areacirc  36569  fnopabco  36579  heiborlem8  36674  rngoi  36755  drngoi  36807  ldualvsub  38013  dalemrotyz  38517  dalem6  38527  dalem7  38528  dalem11  38533  dalem12  38534  dalemrotps  38550  dalem30  38561  dalem35  38566  cdleme1  39086  cdleme9  39112  cdleme20c  39170  cdleme20d  39171  cdlemefrs29clN  39258  cdleme37m  39321  cdleme43aN  39348  cdlemg1b2  39430  cdlemg4f  39474  cdlemh2  39675  erngdvlem1  39847  erngdvlem2N  39848  erngdvlem3  39849  erngdvlem4  39850  erngdvlem1-rN  39855  erngdvlem2-rN  39856  erngdvlem3-rN  39857  erngdvlem4-rN  39858  dvh4dimN  40306  lcdvsub  40476  hlhilsca  40794  hlhilbase  40795  hlhilplus  40796  hlhilvsca  40810  hlhilip  40811  hlhilipval  40812  rnasclg  41070  evlsval3  41128  reelznn0nn  41318  prjspeclsp  41350  mzpcompact2lem  41474  eldioph2lem1  41483  fiphp3d  41542  rmxypairf1o  41635  wopprc  41754  lmhmlnmsplit  41814  rp-tfslim  42088  onsucunitp  42108  clcnvlem  42359  mnringnmulrd  42953  mnringnmulrdOLD  42954  mnringbaserd  42957  mnringmulrd  42965  dmmptdff  43907  dmmptdf2  43920  ellimcabssub0  44319  cosknegpi  44571  fourierdlem58  44866  fourierdlem59  44867  fourierdlem72  44880  fourierdlem80  44888  sqwvfourb  44931  etransclem28  44964  etransclem41  44977  omef  45198  dfaimafn  45859  afv2co2  45951  sbgoldbo  46441  rrxlinesc  47374  rrxlinec  47375  rrx2linest2  47383  rrxsphere  47387  itsclinecirc0b  47413  itsclquadb  47415  prstcnid  47639  prstcthin  47649