Theorem eqtr4id 2793

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  rabeqcda  3444  iftrue  4536  iffalse  4539  difprsn1  4804  dmmptg  6263  setlikespec  6347  funimacnv  6648  dmmptd  6713  resasplit  6778  dffv3  6902  dfimafn  6970  fniinfv  6986  dffv2  7003  fvco2  7005  fniunfv  7266  isoini  7357  fvmpopr2d  7594  zfrep6  7977  oprabco  8119  suppco  8229  oeeulem  8637  ixpconstg  8944  sbthlem4  9124  sbthlem5  9125  sbthlem6  9126  supval2  9492  hartogslem1  9579  cantnflem1d  9725  alephsuc2  10117  dfac3  10158  hsmexlem5  10467  axdc2lem  10485  gruima  10839  eqneg  11984  zeo  12701  fseq1p1m1  13634  hashfzo  14464  hashimarn  14475  wrdval  14551  wrdnval  14579  repswswrd  14818  s1co  14868  swrds2  14975  s7f1o  15001  modfsummod  15826  telfsumo  15834  mulgcd  16581  algcvg  16609  phiprmpw  16809  phisum  16823  strfv3  17238  resseqnbas  17286  resslemOLD  17287  pwssnf1o  17544  imassca  17565  homfeq  17738  oppcbas  17763  oppcbasOLD  17764  resscatc  18162  estrcbasbas  18185  funcestrcsetclem7  18201  funcestrcsetclem8  18202  funcestrcsetclem9  18203  fthestrcsetc  18205  fullestrcsetc  18206  equivestrcsetc  18207  setc1strwun  18208  funcsetcestrclem7  18216  funcsetcestrclem8  18217  funcsetcestrclem9  18218  fthsetcestrc  18220  fullsetcestrc  18221  lubsn  18539  ipotset  18590  ipole  18591  plusfeq  18673  pws0g  18798  frmd0  18885  efmndtset  18904  oppgplusfval  19378  gsmsymgrfix  19460  gsmsymgreq  19464  psgnunilem2  19527  sylow3lem2  19660  oppglsm  19674  frgpuplem  19804  frgpupf  19805  frgpup1  19807  frgpup3lem  19809  gsumzoppg  19976  ablfac1eu  20107  pgpfaclem1  20115  pwsmgp  20340  opprmulfval  20352  rdivmuldivd  20429  dfrhm2  20490  subrg1  20598  staffn  20860  issrngd  20872  scafeq  20896  lbsextlem4  21180  sralem  21192  sralemOLD  21193  sravsca  21202  sravscaOLD  21203  sraip  21204  2idlbas  21290  zlmlem  21544  zlmlemOLD  21545  zlmvsca  21553  znbaslem  21570  znbaslemOLD  21571  ipfeq  21685  ssipeq  21691  thlbas  21731  thlbasOLD  21732  thlle  21733  thlleOLD  21734  thloc  21736  dsmmbase  21772  dsmmelbas  21776  frlmelbas  21793  frlmphl  21818  islindf4  21875  rnascl  21928  psrlinv  21992  opsrbaslem  22084  opsrbaslemOLD  22085  evlseu  22124  mpfsubrg  22144  ply1scl0OLD  22309  evl1sca  22353  evls1var  22357  matbas  22432  matplusg  22433  matsca  22434  matscaOLD  22435  matvsca  22436  matvscaOLD  22437  matbas2d  22444  matsubgcell  22455  matmulcell  22466  ofco2  22472  mattposm  22480  mat1f1o  22499  mdetunilem8  22640  madugsum  22664  cramerimplem2  22705  decpmatmullem  22792  paste  23317  ptpjcn  23634  uptx  23648  xpstopnlem1  23832  alexsubALTlem4  24073  cnextf  24089  submtmd  24127  ussval  24283  tuslem  24290  tuslemOLD  24291  psmetge0  24337  xmetge0  24369  setsmsds  24502  setsmsdsOLD  24503  sgrim  24659  tnglem  24668  tnglemOLD  24669  tngtset  24685  tngngp2  24688  resubmet  24837  pcorev2  25074  om1plusg  25080  om1tset  25081  om1opn  25082  pi1grplem  25095  clmadd  25120  clmmul  25121  clmcj  25122  tcphtopn  25273  tchnmfval  25275  bcthlem1  25371  bcthlem2  25372  bcthlem4  25374  bcth3  25378  rrxmval  25452  rrxmfval  25453  rrxdsfi  25458  ehlbase  25462  minveclem3b  25475  pjthlem1  25484  volun  25593  voliun  25602  uniioovol  25627  itg2i1fseq  25804  itgcnlem  25839  iblabslem  25877  limcres  25935  cnplimc  25936  ply1termlem  26256  0dgr  26298  taylthlem1  26429  abelth  26499  lawcos  26873  lgambdd  27094  basellem8  27145  musum  27248  chtub  27270  dchrval  27292  dchrinvcl  27311  lgsval4lem  27366  lgsquadlem2  27439  m1lgs  27446  cuteq0  27891  precsexlem11  28255  seqsval  28308  n0sbday  28368  zseo  28420  mirauto  28706  lmiisolem  28818  ttglem  28899  ttglemOLD  28900  axlowdimlem16  28986  ebtwntg  29011  ecgrtg  29012  elntg2  29014  nbgrval  29367  uvtxupgrres  29439  clwlknf1oclwwlknlem3  30111  eucrct2eupth  30273  smcnlem  30725  siii  30881  pjhthlem1  31419  sbcies  32515  imadifxp  32620  dfimafnf  32652  funcnvmpt  32683  ccatws1f1olast  32921  gsumwun  33050  symgcom  33085  cycpmconjslem1  33156  rloc0g  33257  rloc1r  33258  resvlem  33336  resvlemOLD  33337  qusker  33356  elrspunsn  33436  opprqusplusg  33496  idlsrgbas  33511  idlsrgplusg  33512  idlsrgmulr  33514  idlsrgtset  33515  idlsrgmulrval  33516  irredminply  33721  algextdeglem4  33725  algextdeglem5  33726  constrrtcc  33740  mdetpmtr12  33785  zarcls  33834  zar0ring  33838  pstmval  33855  xpinpreima2  33867  pnfneige0  33911  zlmds  33922  zlmdsOLD  33923  zlmtset  33924  zlmtsetOLD  33925  esumid  34024  esumrnmpt  34032  sxsigon  34172  carsgclctunlem1  34298  circlemethnat  34634  fnrelpredd  35081  f1resfz0f1d  35097  pthhashvtx  35111  filnetlem4  36363  setsstrset  37118  finxpreclem4  37376  itg2addnclem  37657  iblabsnclem  37669  areacirc  37699  fnopabco  37709  heiborlem8  37804  rngoi  37885  drngoi  37937  ldualvsub  39136  dalemrotyz  39640  dalem6  39650  dalem7  39651  dalem11  39656  dalem12  39657  dalemrotps  39673  dalem30  39684  dalem35  39689  cdleme1  40209  cdleme9  40235  cdleme20c  40293  cdleme20d  40294  cdlemefrs29clN  40381  cdleme37m  40444  cdleme43aN  40471  cdlemg1b2  40553  cdlemg4f  40597  cdlemh2  40798  erngdvlem1  40970  erngdvlem2N  40971  erngdvlem3  40972  erngdvlem4  40973  erngdvlem1-rN  40978  erngdvlem2-rN  40979  erngdvlem3-rN  40980  erngdvlem4-rN  40981  dvh4dimN  41429  lcdvsub  41599  hlhilsca  41917  hlhilbase  41918  hlhilplus  41919  hlhilvsca  41933  hlhilip  41934  hlhilipval  41935  reelznn0nn  42455  rnasclg  42485  evlsval3  42545  prjspeclsp  42598  mzpcompact2lem  42738  eldioph2lem1  42747  fiphp3d  42806  rmxypairf1o  42899  wopprc  43018  lmhmlnmsplit  43075  rp-tfslim  43342  onsucunitp  43362  clcnvlem  43612  mnringnmulrd  44204  mnringnmulrdOLD  44205  mnringbaserd  44208  mnringmulrd  44216  dmmptdff  45165  dmmptdf2  45175  ellimcabssub0  45572  cosknegpi  45824  dvnprodlem1  45901  fourierdlem58  46119  fourierdlem59  46120  fourierdlem72  46133  fourierdlem80  46141  sqwvfourb  46184  etransclem28  46217  etransclem41  46230  omef  46451  dfaimafn  47114  afv2co2  47206  sbgoldbo  47711  rrxlinesc  48584  rrxlinec  48585  rrx2linest2  48593  rrxsphere  48597  itsclinecirc0b  48623  itsclquadb  48625  prstcnid  48866  prstcthin  48876