Theorem eqtr4id 2791

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

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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabeqcda  3412  iftrue  4487  iffalse  4490  difprsn1  4758  dmmptg  6208  setlikespec  6291  funimacnv  6581  dmmptd  6645  resasplit  6712  dffv3  6838  dfimafn  6904  fniinfv  6920  dffv2  6937  fvco2  6939  funcnvmpt  6951  fniunfv  7203  isoini  7294  fvmpopr2d  7530  zfrep6  7909  oprabco  8048  suppco  8158  oeeulem  8539  ixpconstg  8856  sbthlem4  9030  sbthlem5  9031  sbthlem6  9032  supval2  9370  hartogslem1  9459  cantnflem1d  9609  alephsuc2  10002  dfac3  10043  hsmexlem5  10352  axdc2lem  10370  gruima  10725  eqneg  11873  zeo  12590  fseq1p1m1  13526  hashfzo  14364  hashimarn  14375  wrdval  14451  wrdnval  14480  repswswrd  14719  s1co  14768  swrds2  14875  s7f1o  14901  modfsummod  15729  telfsumo  15737  mulgcd  16487  algcvg  16515  phiprmpw  16715  phisum  16730  strfv3  17143  resseqnbas  17181  pwssnf1o  17431  imassca  17452  homfeq  17629  oppcbas  17653  resscatc  18045  estrcbasbas  18066  funcestrcsetclem7  18081  funcestrcsetclem8  18082  funcestrcsetclem9  18083  fthestrcsetc  18085  fullestrcsetc  18086  equivestrcsetc  18087  setc1strwun  18088  funcsetcestrclem7  18096  funcsetcestrclem8  18097  funcsetcestrclem9  18098  fthsetcestrc  18100  fullsetcestrc  18101  lubsn  18417  ipotset  18468  ipole  18469  plusfeq  18585  pws0g  18710  frmd0  18797  efmndtset  18816  oppgplusfval  19289  gsmsymgrfix  19369  gsmsymgreq  19373  psgnunilem2  19436  sylow3lem2  19569  oppglsm  19583  frgpuplem  19713  frgpupf  19714  frgpup1  19716  frgpup3lem  19718  gsumzoppg  19885  ablfac1eu  20016  pgpfaclem1  20024  pwsmgp  20274  opprmulfval  20287  rdivmuldivd  20361  dfrhm2  20422  subrg1  20527  staffn  20788  issrngd  20800  scafeq  20845  lbsextlem4  21128  sralem  21140  sravsca  21145  sraip  21146  2idlbas  21230  zlmlem  21483  zlmvsca  21488  znbaslem  21505  ipfeq  21617  ssipeq  21623  thlbas  21663  thlle  21664  thloc  21666  dsmmbase  21702  dsmmelbas  21706  frlmelbas  21723  frlmphl  21748  islindf4  21805  rnascl  21859  psrlinv  21923  opsrbaslem  22016  evlseu  22050  evlsval3  22056  mpfsubrg  22078  psdmvr  22124  ply1scl0OLD  22245  evl1sca  22290  evls1var  22294  matbas  22369  matplusg  22370  matsca  22371  matvsca  22372  matbas2d  22379  matsubgcell  22390  matmulcell  22401  ofco2  22407  mattposm  22415  mat1f1o  22434  mdetunilem8  22575  madugsum  22599  cramerimplem2  22640  decpmatmullem  22727  paste  23250  ptpjcn  23567  uptx  23581  xpstopnlem1  23765  alexsubALTlem4  24006  cnextf  24022  submtmd  24060  ussval  24215  tuslem  24222  psmetge0  24268  xmetge0  24300  setsmsds  24432  sgrim  24587  tnglem  24596  tngtset  24605  tngngp2  24608  resubmet  24758  pcorev2  24996  om1plusg  25002  om1tset  25003  om1opn  25004  pi1grplem  25017  clmadd  25042  clmmul  25043  clmcj  25044  tcphtopn  25194  tchnmfval  25196  bcthlem1  25292  bcthlem2  25293  bcthlem4  25295  bcth3  25299  rrxmval  25373  rrxmfval  25374  rrxdsfi  25379  ehlbase  25383  minveclem3b  25396  pjthlem1  25405  volun  25514  voliun  25523  uniioovol  25548  itg2i1fseq  25724  itgcnlem  25759  iblabslem  25797  limcres  25855  cnplimc  25856  ply1termlem  26176  0dgr  26218  taylthlem1  26349  abelth  26419  lawcos  26794  lgambdd  27015  basellem8  27066  musum  27169  chtub  27191  dchrval  27213  dchrinvcl  27232  lgsval4lem  27287  lgsquadlem2  27360  m1lgs  27367  cuteq0  27823  precsexlem11  28225  seqsval  28296  n0bday  28360  zseo  28430  mirauto  28768  lmiisolem  28880  ttglem  28960  axlowdimlem16  29042  ebtwntg  29067  ecgrtg  29068  elntg2  29070  nbgrval  29421  uvtxupgrres  29493  clwlknf1oclwwlknlem3  30170  eucrct2eupth  30332  smcnlem  30784  siii  30940  pjhthlem1  31478  sbcies  32573  imadifxp  32687  dfimafnf  32725  ccatws1f1olast  33044  gsummulsubdishift1  33161  gsumwun  33169  symgcom  33176  cycpmconjslem1  33247  rloc0g  33364  rloc1r  33365  resvlem  33425  qusker  33441  elrspunsn  33521  opprqusplusg  33581  idlsrgbas  33596  idlsrgplusg  33597  idlsrgmulr  33599  idlsrgtset  33600  idlsrgmulrval  33601  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  irredminply  33893  algextdeglem4  33897  algextdeglem5  33898  constrrtcc  33912  cos9thpinconstrlem1  33966  mdetpmtr12  34002  zarcls  34051  zar0ring  34055  pstmval  34072  xpinpreima2  34084  pnfneige0  34128  zlmds  34139  zlmtset  34140  esumid  34221  esumrnmpt  34229  sxsigon  34369  carsgclctunlem1  34494  circlemethnat  34818  fnrelpredd  35266  f1resfz0f1d  35327  pthhashvtx  35341  filnetlem4  36594  setsstrset  37380  finxpreclem4  37638  itg2addnclem  37911  iblabsnclem  37923  areacirc  37953  fnopabco  37963  heiborlem8  38058  rngoi  38139  drngoi  38191  ldualvsub  39520  dalemrotyz  40023  dalem6  40033  dalem7  40034  dalem11  40039  dalem12  40040  dalemrotps  40056  dalem30  40067  dalem35  40072  cdleme1  40592  cdleme9  40618  cdleme20c  40676  cdleme20d  40677  cdlemefrs29clN  40764  cdleme37m  40827  cdleme43aN  40854  cdlemg1b2  40936  cdlemg4f  40980  cdlemh2  41181  erngdvlem1  41353  erngdvlem2N  41354  erngdvlem3  41355  erngdvlem4  41356  erngdvlem1-rN  41361  erngdvlem2-rN  41362  erngdvlem3-rN  41363  erngdvlem4-rN  41364  dvh4dimN  41812  lcdvsub  41982  hlhilsca  42300  hlhilbase  42301  hlhilplus  42302  hlhilvsca  42312  hlhilip  42313  hlhilipval  42314  reelznn0nn  42820  rnasclg  42858  prjspeclsp  42959  mzpcompact2lem  43097  eldioph2lem1  43106  fiphp3d  43165  rmxypairf1o  43257  wopprc  43376  lmhmlnmsplit  43433  rp-tfslim  43699  onsucunitp  43719  clcnvlem  43968  mnringnmulrd  44559  mnringbaserd  44561  mnringmulrd  44568  dmmptdff  45570  dmmptdf2  45580  ellimcabssub0  45966  cosknegpi  46216  dvnprodlem1  46293  fourierdlem58  46511  fourierdlem59  46512  fourierdlem72  46525  fourierdlem80  46533  sqwvfourb  46576  etransclem28  46609  etransclem41  46622  omef  46843  dfaimafn  47514  afv2co2  47606  sbgoldbo  48136  rrxlinesc  49084  rrxlinec  49085  rrx2linest2  49093  rrxsphere  49097  itsclinecirc0b  49123  itsclquadb  49125  2oppf  49480  idfullsubc  49509  oppc1stf  49636  oppc2ndf  49637  dfinito4  49849  prstcnid  49901  prstcthin  49909