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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabeqcda  3401  iftrue  4473  iffalse  4476  difprsn1  4746  dmmptg  6207  setlikespec  6290  funimacnv  6580  dmmptd  6644  resasplit  6711  dffv3  6837  dfimafn  6903  fniinfv  6919  dffv2  6936  fvco2  6938  funcnvmpt  6950  fniunfv  7202  isoini  7293  fvmpopr2d  7529  zfrep6OLD  7908  oprabco  8046  suppco  8156  oeeulem  8537  ixpconstg  8854  sbthlem4  9028  sbthlem5  9029  sbthlem6  9030  supval2  9368  hartogslem1  9457  cantnflem1d  9609  alephsuc2  10002  dfac3  10043  hsmexlem5  10352  axdc2lem  10370  gruima  10725  eqneg  11875  zeo  12615  fseq1p1m1  13552  hashfzo  14391  hashimarn  14402  wrdval  14478  wrdnval  14507  repswswrd  14746  s1co  14795  swrds2  14902  s7f1o  14928  modfsummod  15757  telfsumo  15765  indsumhash  15792  mulgcd  16517  algcvg  16545  phiprmpw  16746  phisum  16761  strfv3  17174  resseqnbas  17212  pwssnf1o  17462  imassca  17483  homfeq  17660  oppcbas  17684  resscatc  18076  estrcbasbas  18097  funcestrcsetclem7  18112  funcestrcsetclem8  18113  funcestrcsetclem9  18114  fthestrcsetc  18116  fullestrcsetc  18117  equivestrcsetc  18118  setc1strwun  18119  funcsetcestrclem7  18127  funcsetcestrclem8  18128  funcsetcestrclem9  18129  fthsetcestrc  18131  fullsetcestrc  18132  lubsn  18448  ipotset  18499  ipole  18500  plusfeq  18616  pws0g  18741  frmd0  18828  efmndtset  18847  oppgplusfval  19323  gsmsymgrfix  19403  gsmsymgreq  19407  psgnunilem2  19470  sylow3lem2  19603  oppglsm  19617  frgpuplem  19747  frgpupf  19748  frgpup1  19750  frgpup3lem  19752  gsumzoppg  19919  ablfac1eu  20050  pgpfaclem1  20058  pwsmgp  20306  opprmulfval  20319  rdivmuldivd  20393  dfrhm2  20454  subrg1  20559  staffn  20820  issrngd  20832  scafeq  20877  lbsextlem4  21159  sralem  21171  sravsca  21176  sraip  21177  2idlbas  21261  zlmlem  21496  zlmvsca  21501  znbaslem  21518  ipfeq  21630  ssipeq  21636  thlbas  21676  thlle  21677  thloc  21679  dsmmbase  21715  dsmmelbas  21719  frlmelbas  21736  frlmphl  21761  islindf4  21818  rnascl  21871  psrlinv  21934  opsrbaslem  22027  evlseu  22061  evlsval3  22067  mpfsubrg  22089  psdmvr  22135  evl1sca  22299  evls1var  22303  matbas  22378  matplusg  22379  matsca  22380  matvsca  22381  matbas2d  22388  matsubgcell  22399  matmulcell  22410  ofco2  22416  mattposm  22424  mat1f1o  22443  mdetunilem8  22584  madugsum  22608  cramerimplem2  22649  decpmatmullem  22736  paste  23259  ptpjcn  23576  uptx  23590  xpstopnlem1  23774  alexsubALTlem4  24015  cnextf  24031  submtmd  24069  ussval  24224  tuslem  24231  psmetge0  24277  xmetge0  24309  setsmsds  24441  sgrim  24596  tnglem  24605  tngtset  24614  tngngp2  24617  resubmet  24767  pcorev2  24995  om1plusg  25001  om1tset  25002  om1opn  25003  pi1grplem  25016  clmadd  25041  clmmul  25042  clmcj  25043  tcphtopn  25193  tchnmfval  25195  bcthlem1  25291  bcthlem2  25292  bcthlem4  25294  bcth3  25298  rrxmval  25372  rrxmfval  25373  rrxdsfi  25378  ehlbase  25382  minveclem3b  25395  pjthlem1  25404  volun  25512  voliun  25521  uniioovol  25546  itg2i1fseq  25722  itgcnlem  25757  iblabslem  25795  limcres  25853  cnplimc  25854  ply1termlem  26168  0dgr  26210  taylthlem1  26338  abelth  26406  lawcos  26780  lgambdd  27000  basellem8  27051  musum  27154  chtub  27175  dchrval  27197  dchrinvcl  27216  lgsval4lem  27271  lgsquadlem2  27344  m1lgs  27351  cuteq0  27807  precsexlem11  28209  seqsval  28280  n0bday  28344  zseo  28414  mirauto  28752  lmiisolem  28864  ttglem  28944  axlowdimlem16  29026  ebtwntg  29051  ecgrtg  29052  elntg2  29054  nbgrval  29405  uvtxupgrres  29477  clwlknf1oclwwlknlem3  30153  eucrct2eupth  30315  smcnlem  30768  siii  30924  pjhthlem1  31462  sbcies  32557  imadifxp  32671  dfimafnf  32709  ccatws1f1olast  33012  gsummulsubdishift1  33129  gsumwun  33137  symgcom  33144  cycpmconjslem1  33215  rloc0g  33332  rloc1r  33333  resvlem  33393  qusker  33409  elrspunsn  33489  opprqusplusg  33549  idlsrgbas  33564  idlsrgplusg  33565  idlsrgmulr  33567  idlsrgtset  33568  idlsrgmulrval  33569  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  irredminply  33860  algextdeglem4  33864  algextdeglem5  33865  constrrtcc  33879  cos9thpinconstrlem1  33933  mdetpmtr12  33969  zarcls  34018  zar0ring  34022  pstmval  34039  xpinpreima2  34051  pnfneige0  34095  zlmds  34106  zlmtset  34107  esumid  34188  esumrnmpt  34196  sxsigon  34336  carsgclctunlem1  34461  circlemethnat  34785  fnrelpredd  35234  f1resfz0f1d  35296  pthhashvtx  35310  filnetlem4  36563  setsstrset  37448  finxpreclem4  37710  itg2addnclem  37992  iblabsnclem  38004  areacirc  38034  fnopabco  38044  heiborlem8  38139  rngoi  38220  drngoi  38272  ldualvsub  39601  dalemrotyz  40104  dalem6  40114  dalem7  40115  dalem11  40120  dalem12  40121  dalemrotps  40137  dalem30  40148  dalem35  40153  cdleme1  40673  cdleme9  40699  cdleme20c  40757  cdleme20d  40758  cdlemefrs29clN  40845  cdleme37m  40908  cdleme43aN  40935  cdlemg1b2  41017  cdlemg4f  41061  cdlemh2  41262  erngdvlem1  41434  erngdvlem2N  41435  erngdvlem3  41436  erngdvlem4  41437  erngdvlem1-rN  41442  erngdvlem2-rN  41443  erngdvlem3-rN  41444  erngdvlem4-rN  41445  dvh4dimN  41893  lcdvsub  42063  hlhilsca  42381  hlhilbase  42382  hlhilplus  42383  hlhilvsca  42393  hlhilip  42394  hlhilipval  42395  reelznn0nn  42906  rnasclg  42944  prjspeclsp  43045  mzpcompact2lem  43183  eldioph2lem1  43192  fiphp3d  43247  rmxypairf1o  43339  wopprc  43458  lmhmlnmsplit  43515  rp-tfslim  43781  onsucunitp  43801  clcnvlem  44050  mnringnmulrd  44641  mnringbaserd  44643  mnringmulrd  44650  dmmptdff  45652  dmmptdf2  45662  ellimcabssub0  46047  cosknegpi  46297  dvnprodlem1  46374  fourierdlem58  46592  fourierdlem59  46593  fourierdlem72  46606  fourierdlem80  46614  sqwvfourb  46657  etransclem28  46690  etransclem41  46703  omef  46924  dfaimafn  47607  afv2co2  47699  sbgoldbo  48257  rrxlinesc  49205  rrxlinec  49206  rrx2linest2  49214  rrxsphere  49218  itsclinecirc0b  49244  itsclquadb  49246  2oppf  49601  idfullsubc  49630  oppc1stf  49757  oppc2ndf  49758  dfinito4  49970  prstcnid  50022  prstcthin  50030