Theorem eqtr4id 2814

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  rabeqcda  3423  iftrue  4487  iffalse  4490  difprsn1  4762  csbcnv  5863  dmmptg  6243  setlikespec  6328  funimacnv  6621  dmmptd  6684  resasplit  6752  dffv3  6881  dfimafn  6947  fniinfv  6963  dffv2  6980  fvco2  6982  funcnvmpt  6995  fniunfv  7251  isoini  7346  fvmpopr2d  7582  zfrep6OLD  7967  oprabco  8107  suppco  8224  oeeulem  8611  ixpconstg  8935  sbthlem4  9110  sbthlem5  9111  sbthlem6  9112  supval2  9448  hartogslem1  9537  cantnflem1d  9690  alephsuc2  10160  dfac3  10201  hsmexlem5  10509  axdc2lem  10527  gruima  10888  eqneg  12038  zeo  12786  fseq1p1m1  13733  f1resfz0f1d  13928  hashfzo  14575  hashimarn  14586  wrdval  14662  wrdnval  14691  repswswrd  14936  s1co  14985  swrds2  15092  s7f1o  15120  modfsummod  15962  telfsumo  15970  indsumhash  15997  mulgcd  16722  algcvg  16752  phiprmpw  16954  phisum  16969  strfv3  17383  resseqnbas  17421  pwssnf1o  17671  imassca  17692  homfeq  17869  oppcbas  17893  resscatc  18285  estrcbasbas  18306  funcestrcsetclem7  18321  funcestrcsetclem8  18322  funcestrcsetclem9  18323  fthestrcsetc  18325  fullestrcsetc  18326  equivestrcsetc  18327  setc1strwun  18328  funcsetcestrclem7  18336  funcsetcestrclem8  18337  funcsetcestrclem9  18338  fthsetcestrc  18340  fullsetcestrc  18341  lubsn  18657  ipotset  18708  ipole  18709  plusfeq  18825  idressidex0  18861  pws0g  18968  frmd0  19057  efmndtset  19076  oppgplusfval  19563  gsmsymgrfix  19643  gsmsymgreq  19647  psgnunilem2  19710  sylow3lem2  19843  oppglsm  19857  frgpuplem  19987  frgpupf  19988  frgpup1  19990  frgpup3lem  19992  gsumzoppg  20159  ablfac1eu  20290  pgpfaclem1  20298  pwsmgp  20557  opprmulfval  20570  rdivmuldivd  20644  dfrhm2  20705  subrg1  20835  staffn  21101  issrngd  21113  scafeq  21158  lbsextlem4  21440  sralem  21452  sravsca  21457  sraip  21458  2idlbas  21558  zlmlem  21823  zlmvsca  21828  znbaslem  21845  ipfeq  21957  ssipeq  21963  thlbas  22003  thlle  22004  thloc  22006  dsmmbase  22042  dsmmelbas  22046  frlmelbas  22063  frlmphl  22088  islindf4  22145  rnascl  22200  psrlinv  22264  opsrbaslem  22359  evlseu  22393  evlsval3  22399  mpfsubrg  22421  psdmvr  22491  evl1sca  22653  evls1var  22657  matbas  22729  matplusg  22730  matsca  22731  matvsca  22732  matbas2d  22739  matsubgcell  22750  matmulcell  22761  ofco2  22767  mattposm  22775  mat1f1o  22794  mdetunilem8  22935  madugsum  22959  cramerimplem2  23003  decpmatmullem  23090  paste  23613  ptpjcn  23931  uptx  23945  xpstopnlem1  24129  alexsubALTlem4  24370  cnextf  24386  submtmd  24424  ussval  24579  tuslem  24586  psmetge0  24632  xmetge0  24664  setsmsds  24796  sgrim  24951  tnglem  24960  tngtset  24969  tngngp2  24972  resubmet  25122  pcorev2  25350  om1plusg  25356  om1tset  25357  om1opn  25358  pi1grplem  25371  clmadd  25396  clmmul  25397  clmcj  25398  tcphtopn  25548  tchnmfval  25550  bcthlem1  25646  bcthlem2  25647  bcthlem4  25649  bcth3  25653  rrxmval  25727  rrxmfval  25728  rrxdsfi  25733  ehlbase  25737  minveclem3b  25750  pjthlem1  25759  volun  25867  voliun  25876  uniioovol  25901  itg2i1fseq  26077  itgcnlem  26111  iblabslem  26149  limcres  26207  cnplimc  26208  ply1termlem  26522  0dgr  26565  taylthlem1  26701  abelth  26769  lawcos  27145  lgambdd  27365  basellem8  27416  musum  27519  chtub  27540  dchrval  27562  dchrinvcl  27581  lgsval4lem  27636  lgsquadlem2  27709  m1lgs  27716  cuteq0  28202  precsexlem11  28604  seqsval  28675  n0bday  28739  zseo  28809  mirauto  29157  lmiisolem  29302  ttglem  29454  axlowdimlem16  29536  ebtwntg  29561  ecgrtg  29562  elntg2  29564  nbgrval  29918  uvtxupgrres  29990  pthhashvtx  30316  clwlknf1oclwwlknlem3  30675  eucrct2eupth  30847  smcnlem  31300  siii  31456  pjhthlem1  31994  sbcies  33127  imadifxp  33238  dfimafnf  33273  ccatws1f1olast  33558  gsummulsubdishift1  33672  gsumwun  33680  symgcom  33687  cycpmconjslem1  33758  rloc0g  33876  rloc1r  33877  resvlem  33937  qusker  33953  elrspunsn  34022  opprqusplusg  34056  idlsrgbas  34079  idlsrgplusg  34080  idlsrgmulr  34082  idlsrgtset  34083  idlsrgmulrval  34084  fldextrspundgdvdslem  34355  fldextrspundgdvds  34356  irredminply  34391  algextdeglem4  34395  algextdeglem5  34396  constrrtcc  34410  cos9thpinconstrlem1  34464  mdetpmtr12  34500  zarcls  34549  zar0ring  34553  pstmval  34570  xpinpreima2  34582  pnfneige0  34626  zlmds  34637  zlmtset  34638  esumid  34719  esumrnmpt  34727  sxsigon  34868  carsgclctunlem1  34992  circlemethnat  35313  fnrelpredd  35765  filnetlem4  37244  setsstrset  38131  finxpreclem4  38393  itg2addnclem  38665  iblabsnclem  38677  areacirc  38707  fnopabco  38733  heiborlem8  38828  rngoi  38909  drngoi  38961  ldualvsub  40288  dalemrotyz  40791  dalem6  40801  dalem7  40802  dalem11  40807  dalem12  40808  dalemrotps  40824  dalem30  40835  dalem35  40840  cdleme1  41360  cdleme9  41386  cdleme20c  41444  cdleme20d  41445  cdlemefrs29clN  41532  cdleme37m  41595  cdleme43aN  41622  cdlemg1b2  41704  cdlemg4f  41748  cdlemh2  41949  erngdvlem1  42121  erngdvlem2N  42122  erngdvlem3  42123  erngdvlem4  42124  erngdvlem1-rN  42129  erngdvlem2-rN  42130  erngdvlem3-rN  42131  erngdvlem4-rN  42132  dvh4dimN  42580  lcdvsub  42750  hlhilsca  43068  hlhilbase  43069  hlhilplus  43070  hlhilvsca  43080  hlhilip  43081  hlhilipval  43082  25or6to4  43332  reelznn0nn  43601  rnasclg  43639  prjspeclsp  43716  mzpcompact2lem  43838  eldioph2lem1  43847  fiphp3d  43902  rmxypairf1o  43994  wopprc  44113  lmhmlnmsplit  44165  rp-tfslim  44431  onsucunitp  44451  clcnvlem  44699  mnringnmulrd  45288  mnringbaserd  45290  mnringmulrd  45297  dmmptdff  46312  dmmptdf2  46321  ellimcabssub0  46705  cosknegpi  46955  dvnprodlem1  47032  fourierdlem58  47250  fourierdlem59  47251  fourierdlem72  47264  fourierdlem80  47272  sqwvfourb  47315  etransclem28  47348  etransclem41  47361  omef  47582  dfaimafn  48311  afv2co2  48403  sbgoldbo  48961  rrxlinesc  49923  rrxlinec  49924  rrx2linest2  49932  rrxsphere  49936  itsclinecirc0b  49962  itsclquadb  49964  2oppf  50316  idfullsubc  50345  oppc1stf  50472  oppc2ndf  50473  dfinito4  50685  prstcnid  50737  prstcthin  50745