Theorem eqtr4id 2783

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 2738	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2781	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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rabeqcda  3408  iftrue  4484  iffalse  4487  difprsn1  4754  dmmptg  6195  setlikespec  6277  funimacnv  6567  dmmptd  6631  resasplit  6698  dffv3  6822  dfimafn  6889  fniinfv  6905  dffv2  6922  fvco2  6924  fniunfv  7187  isoini  7279  fvmpopr2d  7515  zfrep6  7897  oprabco  8036  suppco  8146  oeeulem  8526  ixpconstg  8840  sbthlem4  9014  sbthlem5  9015  sbthlem6  9016  supval2  9364  hartogslem1  9453  cantnflem1d  9603  alephsuc2  9993  dfac3  10034  hsmexlem5  10343  axdc2lem  10361  gruima  10715  eqneg  11862  zeo  12580  fseq1p1m1  13519  hashfzo  14354  hashimarn  14365  wrdval  14441  wrdnval  14470  repswswrd  14708  s1co  14758  swrds2  14865  s7f1o  14891  modfsummod  15719  telfsumo  15727  mulgcd  16477  algcvg  16505  phiprmpw  16705  phisum  16720  strfv3  17133  resseqnbas  17171  pwssnf1o  17420  imassca  17441  homfeq  17618  oppcbas  17642  resscatc  18034  estrcbasbas  18055  funcestrcsetclem7  18070  funcestrcsetclem8  18071  funcestrcsetclem9  18072  fthestrcsetc  18074  fullestrcsetc  18075  equivestrcsetc  18076  setc1strwun  18077  funcsetcestrclem7  18085  funcsetcestrclem8  18086  funcsetcestrclem9  18087  fthsetcestrc  18089  fullsetcestrc  18090  lubsn  18406  ipotset  18457  ipole  18458  plusfeq  18540  pws0g  18665  frmd0  18752  efmndtset  18771  oppgplusfval  19245  gsmsymgrfix  19325  gsmsymgreq  19329  psgnunilem2  19392  sylow3lem2  19525  oppglsm  19539  frgpuplem  19669  frgpupf  19670  frgpup1  19672  frgpup3lem  19674  gsumzoppg  19841  ablfac1eu  19972  pgpfaclem1  19980  pwsmgp  20230  opprmulfval  20242  rdivmuldivd  20316  dfrhm2  20377  subrg1  20485  staffn  20746  issrngd  20758  scafeq  20803  lbsextlem4  21086  sralem  21098  sravsca  21103  sraip  21104  2idlbas  21188  zlmlem  21441  zlmvsca  21446  znbaslem  21463  ipfeq  21575  ssipeq  21581  thlbas  21621  thlle  21622  thloc  21624  dsmmbase  21660  dsmmelbas  21664  frlmelbas  21681  frlmphl  21706  islindf4  21763  rnascl  21816  psrlinv  21880  opsrbaslem  21972  evlseu  22006  mpfsubrg  22026  psdmvr  22072  ply1scl0OLD  22193  evl1sca  22237  evls1var  22241  matbas  22316  matplusg  22317  matsca  22318  matvsca  22319  matbas2d  22326  matsubgcell  22337  matmulcell  22348  ofco2  22354  mattposm  22362  mat1f1o  22381  mdetunilem8  22522  madugsum  22546  cramerimplem2  22587  decpmatmullem  22674  paste  23197  ptpjcn  23514  uptx  23528  xpstopnlem1  23712  alexsubALTlem4  23953  cnextf  23969  submtmd  24007  ussval  24163  tuslem  24170  psmetge0  24216  xmetge0  24248  setsmsds  24380  sgrim  24535  tnglem  24544  tngtset  24553  tngngp2  24556  resubmet  24706  pcorev2  24944  om1plusg  24950  om1tset  24951  om1opn  24952  pi1grplem  24965  clmadd  24990  clmmul  24991  clmcj  24992  tcphtopn  25142  tchnmfval  25144  bcthlem1  25240  bcthlem2  25241  bcthlem4  25243  bcth3  25247  rrxmval  25321  rrxmfval  25322  rrxdsfi  25327  ehlbase  25331  minveclem3b  25344  pjthlem1  25353  volun  25462  voliun  25471  uniioovol  25496  itg2i1fseq  25672  itgcnlem  25707  iblabslem  25745  limcres  25803  cnplimc  25804  ply1termlem  26124  0dgr  26166  taylthlem1  26297  abelth  26367  lawcos  26742  lgambdd  26963  basellem8  27014  musum  27117  chtub  27139  dchrval  27161  dchrinvcl  27180  lgsval4lem  27235  lgsquadlem2  27308  m1lgs  27315  cuteq0  27764  precsexlem11  28142  seqsval  28205  n0sbday  28267  zseo  28332  mirauto  28647  lmiisolem  28759  ttglem  28839  axlowdimlem16  28920  ebtwntg  28945  ecgrtg  28946  elntg2  28948  nbgrval  29299  uvtxupgrres  29371  clwlknf1oclwwlknlem3  30045  eucrct2eupth  30207  smcnlem  30659  siii  30815  pjhthlem1  31353  sbcies  32450  imadifxp  32563  dfimafnf  32593  funcnvmpt  32624  ccatws1f1olast  32907  gsumwun  33031  symgcom  33038  cycpmconjslem1  33109  rloc0g  33221  rloc1r  33222  resvlem  33281  qusker  33296  elrspunsn  33376  opprqusplusg  33436  idlsrgbas  33451  idlsrgplusg  33452  idlsrgmulr  33454  idlsrgtset  33455  idlsrgmulrval  33456  fldextrspundgdvdslem  33651  fldextrspundgdvds  33652  irredminply  33682  algextdeglem4  33686  algextdeglem5  33687  constrrtcc  33701  cos9thpinconstrlem1  33755  mdetpmtr12  33791  zarcls  33840  zar0ring  33844  pstmval  33861  xpinpreima2  33873  pnfneige0  33917  zlmds  33928  zlmtset  33929  esumid  34010  esumrnmpt  34018  sxsigon  34158  carsgclctunlem1  34284  circlemethnat  34608  fnrelpredd  35055  f1resfz0f1d  35086  pthhashvtx  35100  filnetlem4  36354  setsstrset  37109  finxpreclem4  37367  itg2addnclem  37650  iblabsnclem  37662  areacirc  37692  fnopabco  37702  heiborlem8  37797  rngoi  37878  drngoi  37930  ldualvsub  39133  dalemrotyz  39637  dalem6  39647  dalem7  39648  dalem11  39653  dalem12  39654  dalemrotps  39670  dalem30  39681  dalem35  39686  cdleme1  40206  cdleme9  40232  cdleme20c  40290  cdleme20d  40291  cdlemefrs29clN  40378  cdleme37m  40441  cdleme43aN  40468  cdlemg1b2  40550  cdlemg4f  40594  cdlemh2  40795  erngdvlem1  40967  erngdvlem2N  40968  erngdvlem3  40969  erngdvlem4  40970  erngdvlem1-rN  40975  erngdvlem2-rN  40976  erngdvlem3-rN  40977  erngdvlem4-rN  40978  dvh4dimN  41426  lcdvsub  41596  hlhilsca  41914  hlhilbase  41915  hlhilplus  41916  hlhilvsca  41926  hlhilip  41927  hlhilipval  41928  reelznn0nn  42434  rnasclg  42472  evlsval3  42532  prjspeclsp  42585  mzpcompact2lem  42724  eldioph2lem1  42733  fiphp3d  42792  rmxypairf1o  42884  wopprc  43003  lmhmlnmsplit  43060  rp-tfslim  43326  onsucunitp  43346  clcnvlem  43596  mnringnmulrd  44187  mnringbaserd  44189  mnringmulrd  44196  dmmptdff  45201  dmmptdf2  45211  ellimcabssub0  45599  cosknegpi  45851  dvnprodlem1  45928  fourierdlem58  46146  fourierdlem59  46147  fourierdlem72  46160  fourierdlem80  46168  sqwvfourb  46211  etransclem28  46244  etransclem41  46257  omef  46478  dfaimafn  47150  afv2co2  47242  sbgoldbo  47772  rrxlinesc  48708  rrxlinec  48709  rrx2linest2  48717  rrxsphere  48721  itsclinecirc0b  48747  itsclquadb  48749  2oppf  49105  idfullsubc  49134  oppc1stf  49261  oppc2ndf  49262  dfinito4  49474  prstcnid  49526  prstcthin  49534