Theorem eqtr4id 2815

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

Syntax hints:   → wi 4   = wceq 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753

This theorem is referenced by:  rabeqcda  3425  iftrue  4492  iffalse  4495  difprsn1  4767  csbcnv  5872  dmmptg  6243  setlikespec  6326  funimacnv  6617  dmmptd  6680  resasplit  6748  dffv3  6877  dfimafn  6943  fniinfv  6959  dffv2  6976  fvco2  6978  funcnvmpt  6991  fniunfv  7245  isoini  7336  fvmpopr2d  7572  zfrep6OLD  7951  oprabco  8090  suppco  8201  oeeulem  8586  ixpconstg  8903  sbthlem4  9077  sbthlem5  9078  sbthlem6  9079  supval2  9414  hartogslem1  9503  cantnflem1d  9656  alephsuc2  10063  dfac3  10104  hsmexlem5  10413  axdc2lem  10431  gruima  10786  eqneg  11934  zeo  12681  fseq1p1m1  13626  hashfzo  14466  hashimarn  14477  wrdval  14553  wrdnval  14582  repswswrd  14821  s1co  14870  swrds2  14977  s7f1o  15003  modfsummod  15846  telfsumo  15854  indsumhash  15881  mulgcd  16605  algcvg  16633  phiprmpw  16834  phisum  16849  strfv3  17263  resseqnbas  17301  pwssnf1o  17551  imassca  17572  homfeq  17749  oppcbas  17773  resscatc  18165  estrcbasbas  18186  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  18537  ipotset  18588  ipole  18589  plusfeq  18705  pws0g  18830  frmd0  18918  efmndtset  18937  oppgplusfval  19417  gsmsymgrfix  19497  gsmsymgreq  19501  psgnunilem2  19564  sylow3lem2  19697  oppglsm  19711  frgpuplem  19841  frgpupf  19842  frgpup1  19844  frgpup3lem  19846  gsumzoppg  20013  ablfac1eu  20144  pgpfaclem1  20152  pwsmgp  20407  opprmulfval  20420  rdivmuldivd  20494  dfrhm2  20555  subrg1  20666  staffn  20925  issrngd  20937  scafeq  20982  lbsextlem4  21264  sralem  21276  sravsca  21281  sraip  21282  2idlbas  21381  zlmlem  21645  zlmvsca  21650  znbaslem  21667  ipfeq  21779  ssipeq  21785  thlbas  21825  thlle  21826  thloc  21828  dsmmbase  21864  dsmmelbas  21868  frlmelbas  21885  frlmphl  21910  islindf4  21967  rnascl  22020  psrlinv  22084  opsrbaslem  22179  evlseu  22213  evlsval3  22219  mpfsubrg  22241  psdmvr  22311  evl1sca  22473  evls1var  22477  matbas  22549  matplusg  22550  matsca  22551  matvsca  22552  matbas2d  22559  matsubgcell  22570  matmulcell  22581  ofco2  22587  mattposm  22595  mat1f1o  22614  mdetunilem8  22755  madugsum  22779  cramerimplem2  22820  decpmatmullem  22907  paste  23430  ptpjcn  23747  uptx  23761  xpstopnlem1  23945  alexsubALTlem4  24186  cnextf  24202  submtmd  24240  ussval  24395  tuslem  24402  psmetge0  24448  xmetge0  24480  setsmsds  24612  sgrim  24767  tnglem  24776  tngtset  24785  tngngp2  24788  resubmet  24938  pcorev2  25166  om1plusg  25172  om1tset  25173  om1opn  25174  pi1grplem  25187  clmadd  25212  clmmul  25213  clmcj  25214  tcphtopn  25364  tchnmfval  25366  bcthlem1  25462  bcthlem2  25463  bcthlem4  25465  bcth3  25469  rrxmval  25543  rrxmfval  25544  rrxdsfi  25549  ehlbase  25553  minveclem3b  25566  pjthlem1  25575  volun  25683  voliun  25692  uniioovol  25717  itg2i1fseq  25893  itgcnlem  25928  iblabslem  25966  limcres  26024  cnplimc  26025  ply1termlem  26339  0dgr  26381  taylthlem1  26512  abelth  26580  lawcos  26957  lgambdd  27177  basellem8  27228  musum  27331  chtub  27352  dchrval  27374  dchrinvcl  27393  lgsval4lem  27448  lgsquadlem2  27521  m1lgs  27528  cuteq0  27984  precsexlem11  28386  seqsval  28457  n0bday  28521  zseo  28591  mirauto  28937  lmiisolem  29079  ttglem  29191  axlowdimlem16  29273  ebtwntg  29298  ecgrtg  29299  elntg2  29301  nbgrval  29652  uvtxupgrres  29724  clwlknf1oclwwlknlem3  30400  eucrct2eupth  30562  smcnlem  31015  siii  31171  pjhthlem1  31709  sbcies  32800  imadifxp  32912  dfimafnf  32947  ccatws1f1olast  33238  gsummulsubdishift1  33354  gsumwun  33362  symgcom  33369  cycpmconjslem1  33440  rloc0g  33558  rloc1r  33559  resvlem  33619  qusker  33635  elrspunsn  33703  opprqusplusg  33737  idlsrgbas  33760  idlsrgplusg  33761  idlsrgmulr  33763  idlsrgtset  33764  idlsrgmulrval  33765  fldextrspundgdvdslem  34036  fldextrspundgdvds  34037  irredminply  34072  algextdeglem4  34076  algextdeglem5  34077  constrrtcc  34091  cos9thpinconstrlem1  34145  mdetpmtr12  34181  zarcls  34230  zar0ring  34234  pstmval  34251  xpinpreima2  34263  pnfneige0  34307  zlmds  34318  zlmtset  34319  esumid  34400  esumrnmpt  34408  sxsigon  34548  carsgclctunlem1  34673  circlemethnat  34994  fnrelpredd  35448  f1resfz0f1d  35571  pthhashvtx  35586  filnetlem4  36858  setsstrset  37744  finxpreclem4  38006  itg2addnclem  38288  iblabsnclem  38300  areacirc  38330  fnopabco  38340  heiborlem8  38435  rngoi  38516  drngoi  38568  ldualvsub  39897  dalemrotyz  40400  dalem6  40410  dalem7  40411  dalem11  40416  dalem12  40417  dalemrotps  40433  dalem30  40444  dalem35  40449  cdleme1  40969  cdleme9  40995  cdleme20c  41053  cdleme20d  41054  cdlemefrs29clN  41141  cdleme37m  41204  cdleme43aN  41231  cdlemg1b2  41313  cdlemg4f  41357  cdlemh2  41558  erngdvlem1  41730  erngdvlem2N  41731  erngdvlem3  41732  erngdvlem4  41733  erngdvlem1-rN  41738  erngdvlem2-rN  41739  erngdvlem3-rN  41740  erngdvlem4-rN  41741  dvh4dimN  42189  lcdvsub  42359  hlhilsca  42677  hlhilbase  42678  hlhilplus  42679  hlhilvsca  42689  hlhilip  42690  hlhilipval  42691  25or6to4  42941  reelznn0nn  43203  rnasclg  43241  prjspeclsp  43314  mzpcompact2lem  43452  eldioph2lem1  43461  fiphp3d  43516  rmxypairf1o  43608  wopprc  43727  lmhmlnmsplit  43784  rp-tfslim  44050  onsucunitp  44070  clcnvlem  44319  mnringnmulrd  44908  mnringbaserd  44910  mnringmulrd  44917  dmmptdff  45909  dmmptdf2  45918  ellimcabssub0  46303  cosknegpi  46553  dvnprodlem1  46630  fourierdlem58  46848  fourierdlem59  46849  fourierdlem72  46862  fourierdlem80  46870  sqwvfourb  46913  etransclem28  46946  etransclem41  46959  omef  47180  dfaimafn  47869  afv2co2  47961  sbgoldbo  48519  rrxlinesc  49482  rrxlinec  49483  rrx2linest2  49491  rrxsphere  49495  itsclinecirc0b  49521  itsclquadb  49523  2oppf  49877  idfullsubc  49906  oppc1stf  50033  oppc2ndf  50034  dfinito4  50246  prstcnid  50298  prstcthin  50306