Theorem eqtr4id 2787

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  rabeqcda  3408  iftrue  4482  iffalse  4485  difprsn1  4753  dmmptg  6197  setlikespec  6280  funimacnv  6570  dmmptd  6634  resasplit  6701  dffv3  6827  dfimafn  6893  fniinfv  6909  dffv2  6926  fvco2  6928  fniunfv  7190  isoini  7281  fvmpopr2d  7517  zfrep6  7896  oprabco  8035  suppco  8145  oeeulem  8525  ixpconstg  8839  sbthlem4  9013  sbthlem5  9014  sbthlem6  9015  supval2  9349  hartogslem1  9438  cantnflem1d  9588  alephsuc2  9981  dfac3  10022  hsmexlem5  10331  axdc2lem  10349  gruima  10703  eqneg  11851  zeo  12569  fseq1p1m1  13508  hashfzo  14346  hashimarn  14357  wrdval  14433  wrdnval  14462  repswswrd  14701  s1co  14750  swrds2  14857  s7f1o  14883  modfsummod  15711  telfsumo  15719  mulgcd  16469  algcvg  16497  phiprmpw  16697  phisum  16712  strfv3  17125  resseqnbas  17163  pwssnf1o  17412  imassca  17433  homfeq  17610  oppcbas  17634  resscatc  18026  estrcbasbas  18047  funcestrcsetclem7  18062  funcestrcsetclem8  18063  funcestrcsetclem9  18064  fthestrcsetc  18066  fullestrcsetc  18067  equivestrcsetc  18068  setc1strwun  18069  funcsetcestrclem7  18077  funcsetcestrclem8  18078  funcsetcestrclem9  18079  fthsetcestrc  18081  fullsetcestrc  18082  lubsn  18398  ipotset  18449  ipole  18450  plusfeq  18566  pws0g  18691  frmd0  18778  efmndtset  18797  oppgplusfval  19270  gsmsymgrfix  19350  gsmsymgreq  19354  psgnunilem2  19417  sylow3lem2  19550  oppglsm  19564  frgpuplem  19694  frgpupf  19695  frgpup1  19697  frgpup3lem  19699  gsumzoppg  19866  ablfac1eu  19997  pgpfaclem1  20005  pwsmgp  20255  opprmulfval  20267  rdivmuldivd  20341  dfrhm2  20402  subrg1  20507  staffn  20768  issrngd  20780  scafeq  20825  lbsextlem4  21108  sralem  21120  sravsca  21125  sraip  21126  2idlbas  21210  zlmlem  21463  zlmvsca  21468  znbaslem  21485  ipfeq  21597  ssipeq  21603  thlbas  21643  thlle  21644  thloc  21646  dsmmbase  21682  dsmmelbas  21686  frlmelbas  21703  frlmphl  21728  islindf4  21785  rnascl  21838  psrlinv  21902  opsrbaslem  21994  evlseu  22028  mpfsubrg  22048  psdmvr  22094  ply1scl0OLD  22215  evl1sca  22259  evls1var  22263  matbas  22338  matplusg  22339  matsca  22340  matvsca  22341  matbas2d  22348  matsubgcell  22359  matmulcell  22370  ofco2  22376  mattposm  22384  mat1f1o  22403  mdetunilem8  22544  madugsum  22568  cramerimplem2  22609  decpmatmullem  22696  paste  23219  ptpjcn  23536  uptx  23550  xpstopnlem1  23734  alexsubALTlem4  23975  cnextf  23991  submtmd  24029  ussval  24184  tuslem  24191  psmetge0  24237  xmetge0  24269  setsmsds  24401  sgrim  24556  tnglem  24565  tngtset  24574  tngngp2  24577  resubmet  24727  pcorev2  24965  om1plusg  24971  om1tset  24972  om1opn  24973  pi1grplem  24986  clmadd  25011  clmmul  25012  clmcj  25013  tcphtopn  25163  tchnmfval  25165  bcthlem1  25261  bcthlem2  25262  bcthlem4  25264  bcth3  25268  rrxmval  25342  rrxmfval  25343  rrxdsfi  25348  ehlbase  25352  minveclem3b  25365  pjthlem1  25374  volun  25483  voliun  25492  uniioovol  25517  itg2i1fseq  25693  itgcnlem  25728  iblabslem  25766  limcres  25824  cnplimc  25825  ply1termlem  26145  0dgr  26187  taylthlem1  26318  abelth  26388  lawcos  26763  lgambdd  26984  basellem8  27035  musum  27138  chtub  27160  dchrval  27182  dchrinvcl  27201  lgsval4lem  27256  lgsquadlem2  27329  m1lgs  27336  cuteq0  27786  precsexlem11  28165  seqsval  28228  n0sbday  28290  zseo  28355  mirauto  28672  lmiisolem  28784  ttglem  28864  axlowdimlem16  28946  ebtwntg  28971  ecgrtg  28972  elntg2  28974  nbgrval  29325  uvtxupgrres  29397  clwlknf1oclwwlknlem3  30074  eucrct2eupth  30236  smcnlem  30688  siii  30844  pjhthlem1  31382  sbcies  32478  imadifxp  32592  dfimafnf  32629  funcnvmpt  32660  ccatws1f1olast  32944  gsumwun  33056  symgcom  33063  cycpmconjslem1  33134  rloc0g  33249  rloc1r  33250  resvlem  33309  qusker  33325  elrspunsn  33405  opprqusplusg  33465  idlsrgbas  33480  idlsrgplusg  33481  idlsrgmulr  33483  idlsrgtset  33484  idlsrgmulrval  33485  fldextrspundgdvdslem  33704  fldextrspundgdvds  33705  irredminply  33740  algextdeglem4  33744  algextdeglem5  33745  constrrtcc  33759  cos9thpinconstrlem1  33813  mdetpmtr12  33849  zarcls  33898  zar0ring  33902  pstmval  33919  xpinpreima2  33931  pnfneige0  33975  zlmds  33986  zlmtset  33987  esumid  34068  esumrnmpt  34076  sxsigon  34216  carsgclctunlem1  34341  circlemethnat  34665  fnrelpredd  35113  f1resfz0f1d  35169  pthhashvtx  35183  filnetlem4  36436  setsstrset  37191  finxpreclem4  37449  itg2addnclem  37721  iblabsnclem  37733  areacirc  37763  fnopabco  37773  heiborlem8  37868  rngoi  37949  drngoi  38001  ldualvsub  39264  dalemrotyz  39767  dalem6  39777  dalem7  39778  dalem11  39783  dalem12  39784  dalemrotps  39800  dalem30  39811  dalem35  39816  cdleme1  40336  cdleme9  40362  cdleme20c  40420  cdleme20d  40421  cdlemefrs29clN  40508  cdleme37m  40571  cdleme43aN  40598  cdlemg1b2  40680  cdlemg4f  40724  cdlemh2  40925  erngdvlem1  41097  erngdvlem2N  41098  erngdvlem3  41099  erngdvlem4  41100  erngdvlem1-rN  41105  erngdvlem2-rN  41106  erngdvlem3-rN  41107  erngdvlem4-rN  41108  dvh4dimN  41556  lcdvsub  41726  hlhilsca  42044  hlhilbase  42045  hlhilplus  42046  hlhilvsca  42056  hlhilip  42057  hlhilipval  42058  reelznn0nn  42569  rnasclg  42607  evlsval3  42667  prjspeclsp  42720  mzpcompact2lem  42858  eldioph2lem1  42867  fiphp3d  42926  rmxypairf1o  43018  wopprc  43137  lmhmlnmsplit  43194  rp-tfslim  43460  onsucunitp  43480  clcnvlem  43730  mnringnmulrd  44321  mnringbaserd  44323  mnringmulrd  44330  dmmptdff  45334  dmmptdf2  45344  ellimcabssub0  45731  cosknegpi  45981  dvnprodlem1  46058  fourierdlem58  46276  fourierdlem59  46277  fourierdlem72  46290  fourierdlem80  46298  sqwvfourb  46341  etransclem28  46374  etransclem41  46387  omef  46608  dfaimafn  47279  afv2co2  47371  sbgoldbo  47901  rrxlinesc  48850  rrxlinec  48851  rrx2linest2  48859  rrxsphere  48863  itsclinecirc0b  48889  itsclquadb  48891  2oppf  49247  idfullsubc  49276  oppc1stf  49403  oppc2ndf  49404  dfinito4  49616  prstcnid  49668  prstcthin  49676