Theorem eqtr4id 2799

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  rabeqcda  3455  iftrue  4554  iffalse  4557  difprsn1  4825  dmmptg  6273  setlikespec  6357  funimacnv  6659  dmmptd  6725  resasplit  6791  dffv3  6916  dfimafn  6984  fniinfv  7000  dffv2  7017  fvco2  7019  fniunfv  7284  isoini  7374  fvmpopr2d  7612  zfrep6  7995  oprabco  8137  suppco  8247  oeeulem  8657  ixpconstg  8964  sbthlem4  9152  sbthlem5  9153  sbthlem6  9154  supval2  9524  hartogslem1  9611  cantnflem1d  9757  alephsuc2  10149  dfac3  10190  hsmexlem5  10499  axdc2lem  10517  gruima  10871  eqneg  12014  zeo  12729  fseq1p1m1  13658  hashfzo  14478  hashimarn  14489  wrdval  14565  wrdnval  14593  repswswrd  14832  s1co  14882  swrds2  14989  s7f1o  15015  modfsummod  15842  telfsumo  15850  mulgcd  16595  algcvg  16623  phiprmpw  16823  phisum  16837  strfv3  17252  resseqnbas  17300  resslemOLD  17301  pwssnf1o  17558  imassca  17579  homfeq  17752  oppcbas  17777  oppcbasOLD  17778  resscatc  18176  estrcbasbas  18199  funcestrcsetclem7  18215  funcestrcsetclem8  18216  funcestrcsetclem9  18217  fthestrcsetc  18219  fullestrcsetc  18220  equivestrcsetc  18221  setc1strwun  18222  funcsetcestrclem7  18230  funcsetcestrclem8  18231  funcsetcestrclem9  18232  fthsetcestrc  18234  fullsetcestrc  18235  lubsn  18552  ipotset  18603  ipole  18604  plusfeq  18686  pws0g  18808  frmd0  18895  efmndtset  18914  oppgplusfval  19388  gsmsymgrfix  19470  gsmsymgreq  19474  psgnunilem2  19537  sylow3lem2  19670  oppglsm  19684  frgpuplem  19814  frgpupf  19815  frgpup1  19817  frgpup3lem  19819  gsumzoppg  19986  ablfac1eu  20117  pgpfaclem1  20125  pwsmgp  20350  opprmulfval  20362  rdivmuldivd  20439  dfrhm2  20500  subrg1  20610  staffn  20866  issrngd  20878  scafeq  20902  lbsextlem4  21186  sralem  21198  sralemOLD  21199  sravsca  21208  sravscaOLD  21209  sraip  21210  2idlbas  21296  zlmlem  21550  zlmlemOLD  21551  zlmvsca  21559  znbaslem  21576  znbaslemOLD  21577  ipfeq  21691  ssipeq  21697  thlbas  21737  thlbasOLD  21738  thlle  21739  thlleOLD  21740  thloc  21742  dsmmbase  21778  dsmmelbas  21782  frlmelbas  21799  frlmphl  21824  islindf4  21881  rnascl  21934  psrlinv  21998  opsrbaslem  22090  opsrbaslemOLD  22091  evlseu  22130  mpfsubrg  22150  ply1scl0OLD  22315  evl1sca  22359  evls1var  22363  matbas  22438  matplusg  22439  matsca  22440  matscaOLD  22441  matvsca  22442  matvscaOLD  22443  matbas2d  22450  matsubgcell  22461  matmulcell  22472  ofco2  22478  mattposm  22486  mat1f1o  22505  mdetunilem8  22646  madugsum  22670  cramerimplem2  22711  decpmatmullem  22798  paste  23323  ptpjcn  23640  uptx  23654  xpstopnlem1  23838  alexsubALTlem4  24079  cnextf  24095  submtmd  24133  ussval  24289  tuslem  24296  tuslemOLD  24297  psmetge0  24343  xmetge0  24375  setsmsds  24508  setsmsdsOLD  24509  sgrim  24665  tnglem  24674  tnglemOLD  24675  tngtset  24691  tngngp2  24694  resubmet  24843  pcorev2  25080  om1plusg  25086  om1tset  25087  om1opn  25088  pi1grplem  25101  clmadd  25126  clmmul  25127  clmcj  25128  tcphtopn  25279  tchnmfval  25281  bcthlem1  25377  bcthlem2  25378  bcthlem4  25380  bcth3  25384  rrxmval  25458  rrxmfval  25459  rrxdsfi  25464  ehlbase  25468  minveclem3b  25481  pjthlem1  25490  volun  25599  voliun  25608  uniioovol  25633  itg2i1fseq  25810  itgcnlem  25845  iblabslem  25883  limcres  25941  cnplimc  25942  ply1termlem  26262  0dgr  26304  taylthlem1  26433  abelth  26503  lawcos  26877  lgambdd  27098  basellem8  27149  musum  27252  chtub  27274  dchrval  27296  dchrinvcl  27315  lgsval4lem  27370  lgsquadlem2  27443  m1lgs  27450  cuteq0  27895  precsexlem11  28259  seqsval  28312  n0sbday  28372  zseo  28424  mirauto  28710  lmiisolem  28822  ttglem  28903  ttglemOLD  28904  axlowdimlem16  28990  ebtwntg  29015  ecgrtg  29016  elntg2  29018  nbgrval  29371  uvtxupgrres  29443  clwlknf1oclwwlknlem3  30115  eucrct2eupth  30277  smcnlem  30729  siii  30885  pjhthlem1  31423  sbcies  32516  imadifxp  32623  dfimafnf  32655  funcnvmpt  32685  ccatws1f1olast  32919  symgcom  33076  cycpmconjslem1  33147  rloc0g  33243  rloc1r  33244  resvlem  33322  resvlemOLD  33323  qusker  33342  elrspunsn  33422  opprqusplusg  33482  idlsrgbas  33497  idlsrgplusg  33498  idlsrgmulr  33500  idlsrgtset  33501  idlsrgmulrval  33502  irredminply  33707  algextdeglem4  33711  algextdeglem5  33712  constrrtcc  33726  mdetpmtr12  33771  zarcls  33820  zar0ring  33824  pstmval  33841  xpinpreima2  33853  pnfneige0  33897  zlmds  33908  zlmdsOLD  33909  zlmtset  33910  zlmtsetOLD  33911  esumid  34008  esumrnmpt  34016  sxsigon  34156  carsgclctunlem1  34282  circlemethnat  34618  fnrelpredd  35065  f1resfz0f1d  35081  pthhashvtx  35095  filnetlem4  36347  setsstrset  37102  finxpreclem4  37360  itg2addnclem  37631  iblabsnclem  37643  areacirc  37673  fnopabco  37683  heiborlem8  37778  rngoi  37859  drngoi  37911  ldualvsub  39111  dalemrotyz  39615  dalem6  39625  dalem7  39626  dalem11  39631  dalem12  39632  dalemrotps  39648  dalem30  39659  dalem35  39664  cdleme1  40184  cdleme9  40210  cdleme20c  40268  cdleme20d  40269  cdlemefrs29clN  40356  cdleme37m  40419  cdleme43aN  40446  cdlemg1b2  40528  cdlemg4f  40572  cdlemh2  40773  erngdvlem1  40945  erngdvlem2N  40946  erngdvlem3  40947  erngdvlem4  40948  erngdvlem1-rN  40953  erngdvlem2-rN  40954  erngdvlem3-rN  40955  erngdvlem4-rN  40956  dvh4dimN  41404  lcdvsub  41574  hlhilsca  41892  hlhilbase  41893  hlhilplus  41894  hlhilvsca  41908  hlhilip  41909  hlhilipval  41910  reelznn0nn  42425  rnasclg  42454  evlsval3  42514  prjspeclsp  42567  mzpcompact2lem  42707  eldioph2lem1  42716  fiphp3d  42775  rmxypairf1o  42868  wopprc  42987  lmhmlnmsplit  43044  rp-tfslim  43315  onsucunitp  43335  clcnvlem  43585  mnringnmulrd  44178  mnringnmulrdOLD  44179  mnringbaserd  44182  mnringmulrd  44190  dmmptdff  45130  dmmptdf2  45140  ellimcabssub0  45538  cosknegpi  45790  fourierdlem58  46085  fourierdlem59  46086  fourierdlem72  46099  fourierdlem80  46107  sqwvfourb  46150  etransclem28  46183  etransclem41  46196  omef  46417  dfaimafn  47080  afv2co2  47172  sbgoldbo  47661  rrxlinesc  48469  rrxlinec  48470  rrx2linest2  48478  rrxsphere  48482  itsclinecirc0b  48508  itsclquadb  48510  prstcnid  48733  prstcthin  48743