Theorem eqtr4id 2819

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

Syntax hints:   → wi 4   = wceq 1563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  rabeqcda  3428  iftrue  4489  iffalse  4492  difprsn1  4763  csbcnv  5863  dmmptg  6233  setlikespec  6316  funimacnv  6606  dmmptd  6670  resasplit  6738  dffv3  6867  dfimafn  6933  fniinfv  6949  dffv2  6966  fvco2  6968  funcnvmpt  6981  fniunfv  7235  isoini  7326  fvmpopr2d  7562  zfrep6OLD  7940  oprabco  8079  suppco  8190  oeeulem  8575  ixpconstg  8892  sbthlem4  9066  sbthlem5  9067  sbthlem6  9068  supval2  9403  hartogslem1  9492  cantnflem1d  9645  alephsuc2  10052  dfac3  10093  hsmexlem5  10402  axdc2lem  10420  gruima  10775  eqneg  11926  zeo  12673  fseq1p1m1  13617  hashfzo  14456  hashimarn  14467  wrdval  14543  wrdnval  14572  repswswrd  14811  s1co  14860  swrds2  14967  s7f1o  14993  modfsummod  15836  telfsumo  15844  indsumhash  15871  mulgcd  16596  algcvg  16624  phiprmpw  16825  phisum  16840  strfv3  17254  resseqnbas  17292  pwssnf1o  17542  imassca  17563  homfeq  17740  oppcbas  17764  resscatc  18156  estrcbasbas  18177  funcestrcsetclem7  18192  funcestrcsetclem8  18193  funcestrcsetclem9  18194  fthestrcsetc  18196  fullestrcsetc  18197  equivestrcsetc  18198  setc1strwun  18199  funcsetcestrclem7  18207  funcsetcestrclem8  18208  funcsetcestrclem9  18209  fthsetcestrc  18211  fullsetcestrc  18212  lubsn  18528  ipotset  18579  ipole  18580  plusfeq  18696  pws0g  18821  frmd0  18909  efmndtset  18928  oppgplusfval  19409  gsmsymgrfix  19489  gsmsymgreq  19493  psgnunilem2  19556  sylow3lem2  19689  oppglsm  19703  frgpuplem  19833  frgpupf  19834  frgpup1  19836  frgpup3lem  19838  gsumzoppg  20005  ablfac1eu  20136  pgpfaclem1  20144  pwsmgp  20399  opprmulfval  20412  rdivmuldivd  20486  dfrhm2  20547  subrg1  20658  staffn  20915  issrngd  20927  scafeq  20972  lbsextlem4  21254  sralem  21266  sravsca  21271  sraip  21272  2idlbas  21364  zlmlem  21626  zlmvsca  21631  znbaslem  21648  ipfeq  21760  ssipeq  21766  thlbas  21806  thlle  21807  thloc  21809  dsmmbase  21845  dsmmelbas  21849  frlmelbas  21866  frlmphl  21891  islindf4  21948  rnascl  22001  psrlinv  22065  opsrbaslem  22160  evlseu  22194  evlsval3  22200  mpfsubrg  22222  psdmvr  22292  evl1sca  22455  evls1var  22459  matbas  22531  matplusg  22532  matsca  22533  matvsca  22534  matbas2d  22541  matsubgcell  22552  matmulcell  22563  ofco2  22569  mattposm  22577  mat1f1o  22596  mdetunilem8  22737  madugsum  22761  cramerimplem2  22802  decpmatmullem  22889  paste  23412  ptpjcn  23729  uptx  23743  xpstopnlem1  23927  alexsubALTlem4  24168  cnextf  24184  submtmd  24222  ussval  24377  tuslem  24384  psmetge0  24430  xmetge0  24462  setsmsds  24594  sgrim  24749  tnglem  24758  tngtset  24767  tngngp2  24770  resubmet  24920  pcorev2  25148  om1plusg  25154  om1tset  25155  om1opn  25156  pi1grplem  25169  clmadd  25194  clmmul  25195  clmcj  25196  tcphtopn  25346  tchnmfval  25348  bcthlem1  25444  bcthlem2  25445  bcthlem4  25447  bcth3  25451  rrxmval  25525  rrxmfval  25526  rrxdsfi  25531  ehlbase  25535  minveclem3b  25548  pjthlem1  25557  volun  25665  voliun  25674  uniioovol  25699  itg2i1fseq  25875  itgcnlem  25910  iblabslem  25948  limcres  26006  cnplimc  26007  ply1termlem  26321  0dgr  26363  taylthlem1  26494  abelth  26562  lawcos  26939  lgambdd  27159  basellem8  27210  musum  27313  chtub  27334  dchrval  27356  dchrinvcl  27375  lgsval4lem  27430  lgsquadlem2  27503  m1lgs  27510  cuteq0  27966  precsexlem11  28368  seqsval  28439  n0bday  28503  zseo  28573  mirauto  28915  lmiisolem  29048  ttglem  29134  axlowdimlem16  29216  ebtwntg  29241  ecgrtg  29242  elntg2  29244  nbgrval  29595  uvtxupgrres  29667  clwlknf1oclwwlknlem3  30343  eucrct2eupth  30505  smcnlem  30958  siii  31114  pjhthlem1  31652  sbcies  32744  imadifxp  32856  dfimafnf  32893  ccatws1f1olast  33185  gsummulsubdishift1  33301  gsumwun  33309  symgcom  33316  cycpmconjslem1  33387  rloc0g  33505  rloc1r  33506  resvlem  33568  qusker  33584  elrspunsn  33653  opprqusplusg  33688  idlsrgbas  33711  idlsrgplusg  33712  idlsrgmulr  33714  idlsrgtset  33715  idlsrgmulrval  33716  fldextrspundgdvdslem  33987  fldextrspundgdvds  33988  irredminply  34023  algextdeglem4  34027  algextdeglem5  34028  constrrtcc  34042  cos9thpinconstrlem1  34096  mdetpmtr12  34132  zarcls  34181  zar0ring  34185  pstmval  34202  xpinpreima2  34214  pnfneige0  34258  zlmds  34269  zlmtset  34270  esumid  34351  esumrnmpt  34359  sxsigon  34499  carsgclctunlem1  34624  circlemethnat  34945  fnrelpredd  35397  f1resfz0f1d  35476  pthhashvtx  35491  filnetlem4  36754  setsstrset  37638  finxpreclem4  37900  itg2addnclem  38182  iblabsnclem  38194  areacirc  38224  fnopabco  38234  heiborlem8  38329  rngoi  38410  drngoi  38462  ldualvsub  39791  dalemrotyz  40294  dalem6  40304  dalem7  40305  dalem11  40310  dalem12  40311  dalemrotps  40327  dalem30  40338  dalem35  40343  cdleme1  40863  cdleme9  40889  cdleme20c  40947  cdleme20d  40948  cdlemefrs29clN  41035  cdleme37m  41098  cdleme43aN  41125  cdlemg1b2  41207  cdlemg4f  41251  cdlemh2  41452  erngdvlem1  41624  erngdvlem2N  41625  erngdvlem3  41626  erngdvlem4  41627  erngdvlem1-rN  41632  erngdvlem2-rN  41633  erngdvlem3-rN  41634  erngdvlem4-rN  41635  dvh4dimN  42083  lcdvsub  42253  hlhilsca  42571  hlhilbase  42572  hlhilplus  42573  hlhilvsca  42583  hlhilip  42584  hlhilipval  42585  reelznn0nn  43095  rnasclg  43133  prjspeclsp  43206  mzpcompact2lem  43344  eldioph2lem1  43353  fiphp3d  43408  rmxypairf1o  43500  wopprc  43619  lmhmlnmsplit  43676  rp-tfslim  43942  onsucunitp  43962  clcnvlem  44211  mnringnmulrd  44802  mnringbaserd  44804  mnringmulrd  44811  dmmptdff  45797  dmmptdf2  45806  ellimcabssub0  46191  cosknegpi  46441  dvnprodlem1  46518  fourierdlem58  46736  fourierdlem59  46737  fourierdlem72  46750  fourierdlem80  46758  sqwvfourb  46801  etransclem28  46834  etransclem41  46847  omef  47068  dfaimafn  47757  afv2co2  47849  sbgoldbo  48407  rrxlinesc  49366  rrxlinec  49367  rrx2linest2  49375  rrxsphere  49379  itsclinecirc0b  49405  itsclquadb  49407  2oppf  49761  idfullsubc  49790  oppc1stf  49917  oppc2ndf  49918  dfinito4  50130  prstcnid  50182  prstcthin  50190