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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  rabeqcda  3425  iftrue  4491  iffalse  4494  difprsn1  4766  csbcnv  5870  dmmptg  6242  setlikespec  6327  funimacnv  6618  dmmptd  6681  resasplit  6749  dffv3  6878  dfimafn  6944  fniinfv  6960  dffv2  6977  fvco2  6979  funcnvmpt  6992  fniunfv  7247  isoini  7342  fvmpopr2d  7578  zfrep6OLD  7955  oprabco  8096  suppco  8207  oeeulem  8592  ixpconstg  8916  sbthlem4  9091  sbthlem5  9092  sbthlem6  9093  supval2  9428  hartogslem1  9517  cantnflem1d  9670  alephsuc2  10086  dfac3  10127  hsmexlem5  10435  axdc2lem  10453  gruima  10814  eqneg  11962  zeo  12710  fseq1p1m1  13655  f1resfz0f1d  13850  hashfzo  14496  hashimarn  14507  wrdval  14583  wrdnval  14612  repswswrd  14857  s1co  14906  swrds2  15013  s7f1o  15041  modfsummod  15883  telfsumo  15891  indsumhash  15918  mulgcd  16642  algcvg  16670  phiprmpw  16871  phisum  16886  strfv3  17300  resseqnbas  17338  pwssnf1o  17588  imassca  17609  homfeq  17786  oppcbas  17810  resscatc  18202  estrcbasbas  18223  funcestrcsetclem7  18238  funcestrcsetclem8  18239  funcestrcsetclem9  18240  fthestrcsetc  18242  fullestrcsetc  18243  equivestrcsetc  18244  setc1strwun  18245  funcsetcestrclem7  18253  funcsetcestrclem8  18254  funcsetcestrclem9  18255  fthsetcestrc  18257  fullsetcestrc  18258  lubsn  18574  ipotset  18625  ipole  18626  plusfeq  18742  idressidex0  18777  pws0g  18884  frmd0  18973  efmndtset  18992  oppgplusfval  19479  gsmsymgrfix  19559  gsmsymgreq  19563  psgnunilem2  19626  sylow3lem2  19759  oppglsm  19773  frgpuplem  19903  frgpupf  19904  frgpup1  19906  frgpup3lem  19908  gsumzoppg  20075  ablfac1eu  20206  pgpfaclem1  20214  pwsmgp  20471  opprmulfval  20484  rdivmuldivd  20558  dfrhm2  20619  subrg1  20748  staffn  21013  issrngd  21025  scafeq  21070  lbsextlem4  21352  sralem  21364  sravsca  21369  sraip  21370  2idlbas  21469  zlmlem  21733  zlmvsca  21738  znbaslem  21755  ipfeq  21867  ssipeq  21873  thlbas  21913  thlle  21914  thloc  21916  dsmmbase  21952  dsmmelbas  21956  frlmelbas  21973  frlmphl  21998  islindf4  22055  rnascl  22110  psrlinv  22174  opsrbaslem  22269  evlseu  22303  evlsval3  22309  mpfsubrg  22331  psdmvr  22401  evl1sca  22563  evls1var  22567  matbas  22639  matplusg  22640  matsca  22641  matvsca  22642  matbas2d  22649  matsubgcell  22660  matmulcell  22671  ofco2  22677  mattposm  22685  mat1f1o  22704  mdetunilem8  22845  madugsum  22869  cramerimplem2  22913  decpmatmullem  23000  paste  23523  ptpjcn  23841  uptx  23855  xpstopnlem1  24039  alexsubALTlem4  24280  cnextf  24296  submtmd  24334  ussval  24489  tuslem  24496  psmetge0  24542  xmetge0  24574  setsmsds  24706  sgrim  24861  tnglem  24870  tngtset  24879  tngngp2  24882  resubmet  25032  pcorev2  25260  om1plusg  25266  om1tset  25267  om1opn  25268  pi1grplem  25281  clmadd  25306  clmmul  25307  clmcj  25308  tcphtopn  25458  tchnmfval  25460  bcthlem1  25556  bcthlem2  25557  bcthlem4  25559  bcth3  25563  rrxmval  25637  rrxmfval  25638  rrxdsfi  25643  ehlbase  25647  minveclem3b  25660  pjthlem1  25669  volun  25777  voliun  25786  uniioovol  25811  itg2i1fseq  25987  itgcnlem  26022  iblabslem  26060  limcres  26118  cnplimc  26119  ply1termlem  26433  0dgr  26475  taylthlem1  26609  abelth  26677  lawcos  27054  lgambdd  27274  basellem8  27325  musum  27428  chtub  27449  dchrval  27471  dchrinvcl  27490  lgsval4lem  27545  lgsquadlem2  27618  m1lgs  27625  cuteq0  28081  precsexlem11  28483  seqsval  28554  n0bday  28618  zseo  28688  mirauto  29036  lmiisolem  29181  ttglem  29333  axlowdimlem16  29415  ebtwntg  29440  ecgrtg  29441  elntg2  29443  nbgrval  29797  uvtxupgrres  29869  pthhashvtx  30195  clwlknf1oclwwlknlem3  30554  eucrct2eupth  30726  smcnlem  31179  siii  31335  pjhthlem1  31873  sbcies  32964  imadifxp  33076  dfimafnf  33111  ccatws1f1olast  33396  gsummulsubdishift1  33510  gsumwun  33518  symgcom  33525  cycpmconjslem1  33596  rloc0g  33714  rloc1r  33715  resvlem  33775  qusker  33791  elrspunsn  33859  opprqusplusg  33893  idlsrgbas  33916  idlsrgplusg  33917  idlsrgmulr  33919  idlsrgtset  33920  idlsrgmulrval  33921  fldextrspundgdvdslem  34192  fldextrspundgdvds  34193  irredminply  34228  algextdeglem4  34232  algextdeglem5  34233  constrrtcc  34247  cos9thpinconstrlem1  34301  mdetpmtr12  34337  zarcls  34386  zar0ring  34390  pstmval  34407  xpinpreima2  34419  pnfneige0  34463  zlmds  34474  zlmtset  34475  esumid  34556  esumrnmpt  34564  sxsigon  34705  carsgclctunlem1  34830  circlemethnat  35151  fnrelpredd  35598  filnetlem4  37002  setsstrset  37888  finxpreclem4  38150  itg2addnclem  38422  iblabsnclem  38434  areacirc  38464  fnopabco  38475  heiborlem8  38570  rngoi  38651  drngoi  38703  ldualvsub  40030  dalemrotyz  40533  dalem6  40543  dalem7  40544  dalem11  40549  dalem12  40550  dalemrotps  40566  dalem30  40577  dalem35  40582  cdleme1  41102  cdleme9  41128  cdleme20c  41186  cdleme20d  41187  cdlemefrs29clN  41274  cdleme37m  41337  cdleme43aN  41364  cdlemg1b2  41446  cdlemg4f  41490  cdlemh2  41691  erngdvlem1  41863  erngdvlem2N  41864  erngdvlem3  41865  erngdvlem4  41866  erngdvlem1-rN  41871  erngdvlem2-rN  41872  erngdvlem3-rN  41873  erngdvlem4-rN  41874  dvh4dimN  42322  lcdvsub  42492  hlhilsca  42810  hlhilbase  42811  hlhilplus  42812  hlhilvsca  42822  hlhilip  42823  hlhilipval  42824  25or6to4  43074  reelznn0nn  43351  rnasclg  43389  prjspeclsp  43460  mzpcompact2lem  43598  eldioph2lem1  43607  fiphp3d  43662  rmxypairf1o  43754  wopprc  43873  lmhmlnmsplit  43930  rp-tfslim  44196  onsucunitp  44216  clcnvlem  44465  mnringnmulrd  45054  mnringbaserd  45056  mnringmulrd  45063  dmmptdff  46055  dmmptdf2  46064  ellimcabssub0  46449  cosknegpi  46699  dvnprodlem1  46776  fourierdlem58  46994  fourierdlem59  46995  fourierdlem72  47008  fourierdlem80  47016  sqwvfourb  47059  etransclem28  47092  etransclem41  47105  omef  47326  dfaimafn  48055  afv2co2  48147  sbgoldbo  48705  rrxlinesc  49667  rrxlinec  49668  rrx2linest2  49676  rrxsphere  49680  itsclinecirc0b  49706  itsclquadb  49708  2oppf  50060  idfullsubc  50089  oppc1stf  50216  oppc2ndf  50217  dfinito4  50429  prstcnid  50481  prstcthin  50489