Theorem eqtr4id 2797

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 2795	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  iftrue  4445  iffalse  4448  difprsn1  4713  dmmptg  6105  setlikespec  6183  funimacnv  6461  dmmptd  6523  resasplit  6589  dffv3  6713  dfimafn  6775  fniinfv  6789  dffv2  6806  fvco2  6808  fniunfv  7060  isoini  7147  fvmpopr2d  7370  zfrep6  7728  oprabco  7864  suppco  7948  oeeulem  8329  ixpconstg  8587  sbthlem4  8759  sbthlem5  8760  sbthlem6  8761  supval2  9071  hartogslem1  9158  cantnflem1d  9303  alephsuc2  9694  dfac3  9735  hsmexlem5  10044  axdc2lem  10062  gruima  10416  eqneg  11552  zeo  12263  fseq1p1m1  13186  hashfzo  13996  hashimarn  14007  wrdval  14072  wrdnval  14100  repswswrd  14349  s1co  14398  swrds2  14505  modfsummod  15358  telfsumo  15366  mulgcd  16108  algcvg  16133  phiprmpw  16329  phisum  16343  strfv3  16755  resseqnbas  16793  resslemOLD  16794  pwssnf1o  17003  imassca  17024  homfeq  17197  oppcbas  17222  resscatc  17615  estrcbasbas  17638  funcestrcsetclem7  17653  funcestrcsetclem8  17654  funcestrcsetclem9  17655  fthestrcsetc  17657  fullestrcsetc  17658  equivestrcsetc  17659  setc1strwun  17660  funcsetcestrclem7  17668  funcsetcestrclem8  17669  funcsetcestrclem9  17670  fthsetcestrc  17672  fullsetcestrc  17673  lubsn  17988  ipotset  18039  ipole  18040  plusfeq  18122  pws0g  18209  frmd0  18287  efmndtset  18306  oppgplusfval  18740  gsmsymgrfix  18820  gsmsymgreq  18824  psgnunilem2  18887  sylow3lem2  19017  oppglsm  19031  frgpuplem  19162  frgpupf  19163  frgpup1  19165  frgpup3lem  19167  gsumzoppg  19329  ablfac1eu  19460  pgpfaclem1  19468  pwsmgp  19636  opprmulfval  19643  dfrhm2  19737  subrg1  19810  staffn  19885  issrngd  19897  scafeq  19919  lbsextlem4  20198  sralem  20214  sravsca  20219  sraip  20220  zlmlem  20483  zlmvsca  20488  znbaslem  20503  ipfeq  20612  ssipeq  20618  thlbas  20658  thlle  20659  thloc  20661  dsmmbase  20697  dsmmelbas  20701  frlmelbas  20718  frlmphl  20743  islindf4  20800  rnascl  20851  psrlinv  20922  opsrbaslem  21006  evlseu  21043  mpfsubrg  21063  ply1scl0  21211  evl1sca  21250  evls1var  21254  matbas  21310  matplusg  21311  matsca  21312  matvsca  21313  matbas2d  21320  matsubgcell  21331  matmulcell  21342  ofco2  21348  mattposm  21356  mat1f1o  21375  mdetunilem8  21516  madugsum  21540  cramerimplem2  21581  decpmatmullem  21668  paste  22191  ptpjcn  22508  uptx  22522  xpstopnlem1  22706  alexsubALTlem4  22947  cnextf  22963  submtmd  23001  ussval  23157  tuslem  23164  psmetge0  23210  xmetge0  23242  setsmsds  23374  sgrim  23529  tnglem  23538  tngtset  23547  tngngp2  23550  resubmet  23699  pcorev2  23925  om1plusg  23931  om1tset  23932  om1opn  23933  pi1grplem  23946  clmadd  23971  clmmul  23972  clmcj  23973  tcphtopn  24123  tchnmfval  24125  bcthlem1  24221  bcthlem2  24222  bcthlem4  24224  bcth3  24228  rrxmval  24302  rrxmfval  24303  rrxdsfi  24308  ehlbase  24312  minveclem3b  24325  pjthlem1  24334  volun  24442  voliun  24451  uniioovol  24476  itg2i1fseq  24653  itgcnlem  24687  iblabslem  24725  limcres  24783  cnplimc  24784  ply1termlem  25097  0dgr  25139  taylthlem1  25265  abelth  25333  lawcos  25699  lgambdd  25919  basellem8  25970  musum  26073  chtub  26093  dchrval  26115  dchrinvcl  26134  lgsval4lem  26189  lgsquadlem2  26262  m1lgs  26269  mirauto  26775  lmiisolem  26887  ttglem  26967  axlowdimlem16  27048  ebtwntg  27073  ecgrtg  27074  elntg2  27076  nbgrval  27424  uvtxupgrres  27496  clwlknf1oclwwlknlem3  28166  eucrct2eupth  28328  smcnlem  28778  siii  28934  pjhthlem1  29472  sbcies  30555  imadifxp  30659  dfimafnf  30690  funcnvmpt  30724  symgcom  31071  cycpmconjslem1  31140  rdivmuldivd  31207  resvlem  31249  qusker  31263  idlsrgbas  31363  idlsrgplusg  31364  idlsrgmulr  31366  idlsrgtset  31367  idlsrgmulrval  31368  mdetpmtr12  31489  zarcls  31538  zar0ring  31542  pstmval  31559  xpinpreima2  31571  pnfneige0  31615  zlmds  31626  zlmtset  31627  esumid  31724  esumrnmpt  31732  sxsigon  31872  carsgclctunlem1  31996  circlemethnat  32333  fnrelpredd  32774  f1resfz0f1d  32785  pthhashvtx  32802  filnetlem4  34307  setsstrset  35042  finxpreclem4  35302  itg2addnclem  35565  iblabsnclem  35577  areacirc  35607  fnopabco  35618  heiborlem8  35713  rngoi  35794  drngoi  35846  ldualvsub  36906  dalemrotyz  37409  dalem6  37419  dalem7  37420  dalem11  37425  dalem12  37426  dalemrotps  37442  dalem30  37453  dalem35  37458  cdleme1  37978  cdleme9  38004  cdleme20c  38062  cdleme20d  38063  cdlemefrs29clN  38150  cdleme37m  38213  cdleme43aN  38240  cdlemg1b2  38322  cdlemg4f  38366  cdlemh2  38567  erngdvlem1  38739  erngdvlem2N  38740  erngdvlem3  38741  erngdvlem4  38742  erngdvlem1-rN  38747  erngdvlem2-rN  38748  erngdvlem3-rN  38749  erngdvlem4-rN  38750  dvh4dimN  39198  lcdvsub  39368  hlhilsca  39686  hlhilbase  39687  hlhilplus  39688  hlhilvsca  39698  hlhilip  39699  hlhilipval  39700  rnasclg  39936  evlsval3  39982  evlsbagval  39985  prjspeclsp  40159  mzpcompact2lem  40276  eldioph2lem1  40285  fiphp3d  40344  rmxypairf1o  40436  wopprc  40555  lmhmlnmsplit  40615  clcnvlem  40907  mnringnmulrd  41505  mnringbaserd  41507  mnringmulrd  41514  dmmptdf  42436  dmmptdf2  42449  ellimcabssub0  42833  cosknegpi  43085  fourierdlem58  43380  fourierdlem59  43381  fourierdlem72  43394  fourierdlem80  43402  sqwvfourb  43445  etransclem28  43478  etransclem41  43491  omef  43709  dfaimafn  44329  afv2co2  44421  sbgoldbo  44912  rrxlinesc  45754  rrxlinec  45755  rrx2linest2  45763  rrxsphere  45767  itsclinecirc0b  45793  itsclquadb  45795  prstcnid  46020  prstcthin  46028