MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr4id Structured version   Visualization version   GIF version

Theorem eqtr4id 2796
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
StepHypRef Expression
1 eqtr4id.1 . 2 (𝜑𝐶 = 𝐵)
2 eqtr4id.2 . . 3 𝐴 = 𝐵
32eqcomi 2746 . 2 𝐵 = 𝐴
41, 3eqtr2di 2794 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff setvar class
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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  rabeqcda  3419  iftrue  4493  iffalse  4496  difprsn1  4761  dmmptg  6195  setlikespec  6280  funimacnv  6583  dmmptd  6647  resasplit  6713  dffv3  6839  dfimafn  6906  fniinfv  6920  dffv2  6937  fvco2  6939  fniunfv  7195  isoini  7284  fvmpopr2d  7517  zfrep6  7888  oprabco  8029  suppco  8138  oeeulem  8549  ixpconstg  8845  sbthlem4  9031  sbthlem5  9032  sbthlem6  9033  supval2  9392  hartogslem1  9479  cantnflem1d  9625  alephsuc2  10017  dfac3  10058  hsmexlem5  10367  axdc2lem  10385  gruima  10739  eqneg  11876  zeo  12590  fseq1p1m1  13516  hashfzo  14330  hashimarn  14341  wrdval  14406  wrdnval  14434  repswswrd  14673  s1co  14723  swrds2  14830  modfsummod  15680  telfsumo  15688  mulgcd  16430  algcvg  16453  phiprmpw  16649  phisum  16663  strfv3  17078  resseqnbas  17123  resslemOLD  17124  pwssnf1o  17381  imassca  17402  homfeq  17575  oppcbas  17600  oppcbasOLD  17601  resscatc  17996  estrcbasbas  18019  funcestrcsetclem7  18035  funcestrcsetclem8  18036  funcestrcsetclem9  18037  fthestrcsetc  18039  fullestrcsetc  18040  equivestrcsetc  18041  setc1strwun  18042  funcsetcestrclem7  18050  funcsetcestrclem8  18051  funcsetcestrclem9  18052  fthsetcestrc  18054  fullsetcestrc  18055  lubsn  18372  ipotset  18423  ipole  18424  plusfeq  18506  pws0g  18593  frmd0  18671  efmndtset  18690  oppgplusfval  19127  gsmsymgrfix  19211  gsmsymgreq  19215  psgnunilem2  19278  sylow3lem2  19411  oppglsm  19425  frgpuplem  19555  frgpupf  19556  frgpup1  19558  frgpup3lem  19560  gsumzoppg  19722  ablfac1eu  19853  pgpfaclem1  19861  pwsmgp  20043  opprmulfval  20052  dfrhm2  20149  subrg1  20235  staffn  20311  issrngd  20323  scafeq  20345  lbsextlem4  20625  sralem  20641  sralemOLD  20642  sravsca  20651  sravscaOLD  20652  sraip  20653  zlmlem  20920  zlmlemOLD  20921  zlmvsca  20929  znbaslem  20944  znbaslemOLD  20945  ipfeq  21057  ssipeq  21063  thlbas  21103  thlbasOLD  21104  thlle  21105  thlleOLD  21106  thloc  21108  dsmmbase  21144  dsmmelbas  21148  frlmelbas  21165  frlmphl  21190  islindf4  21247  rnascl  21297  psrlinv  21368  opsrbaslem  21453  opsrbaslemOLD  21454  evlseu  21496  mpfsubrg  21516  ply1scl0  21664  evl1sca  21703  evls1var  21707  matbas  21763  matplusg  21764  matsca  21765  matscaOLD  21766  matvsca  21767  matvscaOLD  21768  matbas2d  21775  matsubgcell  21786  matmulcell  21797  ofco2  21803  mattposm  21811  mat1f1o  21830  mdetunilem8  21971  madugsum  21995  cramerimplem2  22036  decpmatmullem  22123  paste  22648  ptpjcn  22965  uptx  22979  xpstopnlem1  23163  alexsubALTlem4  23404  cnextf  23420  submtmd  23458  ussval  23614  tuslem  23621  tuslemOLD  23622  psmetge0  23668  xmetge0  23700  setsmsds  23833  setsmsdsOLD  23834  sgrim  23990  tnglem  23999  tnglemOLD  24000  tngtset  24016  tngngp2  24019  resubmet  24168  pcorev2  24394  om1plusg  24400  om1tset  24401  om1opn  24402  pi1grplem  24415  clmadd  24440  clmmul  24441  clmcj  24442  tcphtopn  24593  tchnmfval  24595  bcthlem1  24691  bcthlem2  24692  bcthlem4  24694  bcth3  24698  rrxmval  24772  rrxmfval  24773  rrxdsfi  24778  ehlbase  24782  minveclem3b  24795  pjthlem1  24804  volun  24912  voliun  24921  uniioovol  24946  itg2i1fseq  25123  itgcnlem  25157  iblabslem  25195  limcres  25253  cnplimc  25254  ply1termlem  25567  0dgr  25609  taylthlem1  25735  abelth  25803  lawcos  26169  lgambdd  26389  basellem8  26440  musum  26543  chtub  26563  dchrval  26585  dchrinvcl  26604  lgsval4lem  26659  lgsquadlem2  26732  m1lgs  26739  cuteq0  27174  mirauto  27629  lmiisolem  27741  ttglem  27822  ttglemOLD  27823  axlowdimlem16  27909  ebtwntg  27934  ecgrtg  27935  elntg2  27937  nbgrval  28287  uvtxupgrres  28359  clwlknf1oclwwlknlem3  29030  eucrct2eupth  29192  smcnlem  29642  siii  29798  pjhthlem1  30336  sbcies  31419  imadifxp  31522  dfimafnf  31553  funcnvmpt  31586  symgcom  31937  cycpmconjslem1  32006  rdivmuldivd  32074  resvlem  32125  resvlemOLD  32126  qusker  32144  idlsrgbas  32249  idlsrgplusg  32250  idlsrgmulr  32252  idlsrgtset  32253  idlsrgmulrval  32254  mdetpmtr12  32409  zarcls  32458  zar0ring  32462  pstmval  32479  xpinpreima2  32491  pnfneige0  32535  zlmds  32546  zlmdsOLD  32547  zlmtset  32548  zlmtsetOLD  32549  esumid  32646  esumrnmpt  32654  sxsigon  32794  carsgclctunlem1  32920  circlemethnat  33257  fnrelpredd  33696  f1resfz0f1d  33707  pthhashvtx  33724  filnetlem4  34856  setsstrset  35610  finxpreclem4  35868  itg2addnclem  36132  iblabsnclem  36144  areacirc  36174  fnopabco  36185  heiborlem8  36280  rngoi  36361  drngoi  36413  ldualvsub  37620  dalemrotyz  38124  dalem6  38134  dalem7  38135  dalem11  38140  dalem12  38141  dalemrotps  38157  dalem30  38168  dalem35  38173  cdleme1  38693  cdleme9  38719  cdleme20c  38777  cdleme20d  38778  cdlemefrs29clN  38865  cdleme37m  38928  cdleme43aN  38955  cdlemg1b2  39037  cdlemg4f  39081  cdlemh2  39282  erngdvlem1  39454  erngdvlem2N  39455  erngdvlem3  39456  erngdvlem4  39457  erngdvlem1-rN  39462  erngdvlem2-rN  39463  erngdvlem3-rN  39464  erngdvlem4-rN  39465  dvh4dimN  39913  lcdvsub  40083  hlhilsca  40401  hlhilbase  40402  hlhilplus  40403  hlhilvsca  40417  hlhilip  40418  hlhilipval  40419  rnasclg  40677  evlsval3  40747  evlsbagval  40751  reelznn0nn  40921  prjspeclsp  40953  mzpcompact2lem  41077  eldioph2lem1  41086  fiphp3d  41145  rmxypairf1o  41238  wopprc  41357  lmhmlnmsplit  41417  clcnvlem  41902  mnringnmulrd  42496  mnringnmulrdOLD  42497  mnringbaserd  42500  mnringmulrd  42508  dmmptdff  43451  dmmptdf2  43465  ellimcabssub0  43865  cosknegpi  44117  fourierdlem58  44412  fourierdlem59  44413  fourierdlem72  44426  fourierdlem80  44434  sqwvfourb  44477  etransclem28  44510  etransclem41  44523  omef  44744  dfaimafn  45404  afv2co2  45496  sbgoldbo  45986  rrxlinesc  46828  rrxlinec  46829  rrx2linest2  46837  rrxsphere  46841  itsclinecirc0b  46867  itsclquadb  46869  prstcnid  47093  prstcthin  47103
  Copyright terms: Public domain W3C validator