Theorem eqtr4id 2794

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  rabeqcda  3403  iftrue  4467  iffalse  4470  difprsn1  4740  dmmptg  6200  setlikespec  6283  funimacnv  6573  dmmptd  6637  resasplit  6704  dffv3  6830  dfimafn  6896  fniinfv  6912  dffv2  6929  fvco2  6931  funcnvmpt  6944  fniunfv  7198  isoini  7289  fvmpopr2d  7525  zfrep6OLD  7904  oprabco  8042  suppco  8153  oeeulem  8534  ixpconstg  8851  sbthlem4  9025  sbthlem5  9026  sbthlem6  9027  supval2  9365  hartogslem1  9454  cantnflem1d  9607  alephsuc2  10000  dfac3  10041  hsmexlem5  10350  axdc2lem  10368  gruima  10723  eqneg  11873  zeo  12613  fseq1p1m1  13550  hashfzo  14389  hashimarn  14400  wrdval  14476  wrdnval  14505  repswswrd  14744  s1co  14793  swrds2  14900  s7f1o  14926  modfsummod  15755  telfsumo  15763  indsumhash  15790  mulgcd  16515  algcvg  16543  phiprmpw  16744  phisum  16759  strfv3  17172  resseqnbas  17210  pwssnf1o  17460  imassca  17481  homfeq  17658  oppcbas  17682  resscatc  18074  estrcbasbas  18095  funcestrcsetclem7  18110  funcestrcsetclem8  18111  funcestrcsetclem9  18112  fthestrcsetc  18114  fullestrcsetc  18115  equivestrcsetc  18116  setc1strwun  18117  funcsetcestrclem7  18125  funcsetcestrclem8  18126  funcsetcestrclem9  18127  fthsetcestrc  18129  fullsetcestrc  18130  lubsn  18446  ipotset  18497  ipole  18498  plusfeq  18614  pws0g  18739  frmd0  18826  efmndtset  18845  oppgplusfval  19321  gsmsymgrfix  19401  gsmsymgreq  19405  psgnunilem2  19468  sylow3lem2  19601  oppglsm  19615  frgpuplem  19745  frgpupf  19746  frgpup1  19748  frgpup3lem  19750  gsumzoppg  19917  ablfac1eu  20048  pgpfaclem1  20056  pwsmgp  20304  opprmulfval  20317  rdivmuldivd  20391  dfrhm2  20452  subrg1  20561  staffn  20822  issrngd  20834  scafeq  20879  lbsextlem4  21161  sralem  21173  sravsca  21178  sraip  21179  2idlbas  21263  zlmlem  21498  zlmvsca  21503  znbaslem  21520  ipfeq  21632  ssipeq  21638  thlbas  21678  thlle  21679  thloc  21681  dsmmbase  21717  dsmmelbas  21721  frlmelbas  21738  frlmphl  21763  islindf4  21820  rnascl  21873  psrlinv  21937  opsrbaslem  22032  evlseu  22066  evlsval3  22072  mpfsubrg  22094  psdmvr  22164  evl1sca  22327  evls1var  22331  matbas  22403  matplusg  22404  matsca  22405  matvsca  22406  matbas2d  22413  matsubgcell  22424  matmulcell  22435  ofco2  22441  mattposm  22449  mat1f1o  22468  mdetunilem8  22609  madugsum  22633  cramerimplem2  22674  decpmatmullem  22761  paste  23284  ptpjcn  23601  uptx  23615  xpstopnlem1  23799  alexsubALTlem4  24040  cnextf  24056  submtmd  24094  ussval  24249  tuslem  24256  psmetge0  24302  xmetge0  24334  setsmsds  24466  sgrim  24621  tnglem  24630  tngtset  24639  tngngp2  24642  resubmet  24792  pcorev2  25020  om1plusg  25026  om1tset  25027  om1opn  25028  pi1grplem  25041  clmadd  25066  clmmul  25067  clmcj  25068  tcphtopn  25218  tchnmfval  25220  bcthlem1  25316  bcthlem2  25317  bcthlem4  25319  bcth3  25323  rrxmval  25397  rrxmfval  25398  rrxdsfi  25403  ehlbase  25407  minveclem3b  25420  pjthlem1  25429  volun  25537  voliun  25546  uniioovol  25571  itg2i1fseq  25747  itgcnlem  25782  iblabslem  25820  limcres  25878  cnplimc  25879  ply1termlem  26193  0dgr  26235  taylthlem1  26363  abelth  26431  lawcos  26805  lgambdd  27025  basellem8  27076  musum  27179  chtub  27200  dchrval  27222  dchrinvcl  27241  lgsval4lem  27296  lgsquadlem2  27369  m1lgs  27376  cuteq0  27832  precsexlem11  28234  seqsval  28305  n0bday  28369  zseo  28439  mirauto  28777  lmiisolem  28889  ttglem  28969  axlowdimlem16  29051  ebtwntg  29076  ecgrtg  29077  elntg2  29079  nbgrval  29430  uvtxupgrres  29502  clwlknf1oclwwlknlem3  30178  eucrct2eupth  30340  smcnlem  30793  siii  30949  pjhthlem1  31487  sbcies  32582  imadifxp  32697  dfimafnf  32735  ccatws1f1olast  33038  gsummulsubdishift1  33156  gsumwun  33164  symgcom  33171  cycpmconjslem1  33242  rloc0g  33359  rloc1r  33360  resvlem  33423  qusker  33439  elrspunsn  33519  opprqusplusg  33579  idlsrgbas  33594  idlsrgplusg  33595  idlsrgmulr  33597  idlsrgtset  33598  idlsrgmulrval  33599  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  irredminply  33907  algextdeglem4  33911  algextdeglem5  33912  constrrtcc  33926  cos9thpinconstrlem1  33980  mdetpmtr12  34016  zarcls  34065  zar0ring  34069  pstmval  34086  xpinpreima2  34098  pnfneige0  34142  zlmds  34153  zlmtset  34154  esumid  34235  esumrnmpt  34243  sxsigon  34383  carsgclctunlem1  34508  circlemethnat  34832  fnrelpredd  35281  f1resfz0f1d  35343  pthhashvtx  35357  filnetlem4  36610  setsstrset  37495  finxpreclem4  37757  itg2addnclem  38039  iblabsnclem  38051  areacirc  38081  fnopabco  38091  heiborlem8  38186  rngoi  38267  drngoi  38319  ldualvsub  39648  dalemrotyz  40151  dalem6  40161  dalem7  40162  dalem11  40167  dalem12  40168  dalemrotps  40184  dalem30  40195  dalem35  40200  cdleme1  40720  cdleme9  40746  cdleme20c  40804  cdleme20d  40805  cdlemefrs29clN  40892  cdleme37m  40955  cdleme43aN  40982  cdlemg1b2  41064  cdlemg4f  41108  cdlemh2  41309  erngdvlem1  41481  erngdvlem2N  41482  erngdvlem3  41483  erngdvlem4  41484  erngdvlem1-rN  41489  erngdvlem2-rN  41490  erngdvlem3-rN  41491  erngdvlem4-rN  41492  dvh4dimN  41940  lcdvsub  42110  hlhilsca  42428  hlhilbase  42429  hlhilplus  42430  hlhilvsca  42440  hlhilip  42441  hlhilipval  42442  reelznn0nn  42952  rnasclg  42990  prjspeclsp  43063  mzpcompact2lem  43201  eldioph2lem1  43210  fiphp3d  43265  rmxypairf1o  43357  wopprc  43476  lmhmlnmsplit  43533  rp-tfslim  43799  onsucunitp  43819  clcnvlem  44068  mnringnmulrd  44659  mnringbaserd  44661  mnringmulrd  44668  dmmptdff  45669  dmmptdf2  45678  ellimcabssub0  46063  cosknegpi  46313  dvnprodlem1  46390  fourierdlem58  46608  fourierdlem59  46609  fourierdlem72  46622  fourierdlem80  46630  sqwvfourb  46673  etransclem28  46706  etransclem41  46719  omef  46940  dfaimafn  47629  afv2co2  47721  sbgoldbo  48279  rrxlinesc  49227  rrxlinec  49228  rrx2linest2  49236  rrxsphere  49240  itsclinecirc0b  49266  itsclquadb  49268  2oppf  49623  idfullsubc  49652  oppc1stf  49779  oppc2ndf  49780  dfinito4  49992  prstcnid  50044  prstcthin  50052