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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  rabeqcda  3423  iftrue  4487  iffalse  4490  difprsn1  4762  csbcnv  5860  dmmptg  6232  setlikespec  6317  funimacnv  6609  dmmptd  6672  resasplit  6740  dffv3  6869  dfimafn  6935  fniinfv  6951  dffv2  6968  fvco2  6970  funcnvmpt  6983  fniunfv  7239  isoini  7334  fvmpopr2d  7570  zfrep6OLD  7950  oprabco  8090  suppco  8201  oeeulem  8588  ixpconstg  8912  sbthlem4  9087  sbthlem5  9088  sbthlem6  9089  supval2  9425  hartogslem1  9514  cantnflem1d  9667  alephsuc2  10131  dfac3  10172  hsmexlem5  10480  axdc2lem  10498  gruima  10859  eqneg  12007  zeo  12755  fseq1p1m1  13701  f1resfz0f1d  13896  hashfzo  14542  hashimarn  14553  wrdval  14629  wrdnval  14658  repswswrd  14903  s1co  14952  swrds2  15059  s7f1o  15087  modfsummod  15929  telfsumo  15937  indsumhash  15964  mulgcd  16686  algcvg  16714  phiprmpw  16915  phisum  16930  strfv3  17344  resseqnbas  17382  pwssnf1o  17632  imassca  17653  homfeq  17830  oppcbas  17854  resscatc  18246  estrcbasbas  18267  funcestrcsetclem7  18282  funcestrcsetclem8  18283  funcestrcsetclem9  18284  fthestrcsetc  18286  fullestrcsetc  18287  equivestrcsetc  18288  setc1strwun  18289  funcsetcestrclem7  18297  funcsetcestrclem8  18298  funcsetcestrclem9  18299  fthsetcestrc  18301  fullsetcestrc  18302  lubsn  18618  ipotset  18669  ipole  18670  plusfeq  18786  idressidex0  18822  pws0g  18929  frmd0  19018  efmndtset  19037  oppgplusfval  19524  gsmsymgrfix  19604  gsmsymgreq  19608  psgnunilem2  19671  sylow3lem2  19804  oppglsm  19818  frgpuplem  19948  frgpupf  19949  frgpup1  19951  frgpup3lem  19953  gsumzoppg  20120  ablfac1eu  20251  pgpfaclem1  20259  pwsmgp  20518  opprmulfval  20531  rdivmuldivd  20605  dfrhm2  20666  subrg1  20796  staffn  21062  issrngd  21074  scafeq  21119  lbsextlem4  21401  sralem  21413  sravsca  21418  sraip  21419  2idlbas  21519  zlmlem  21784  zlmvsca  21789  znbaslem  21806  ipfeq  21918  ssipeq  21924  thlbas  21964  thlle  21965  thloc  21967  dsmmbase  22003  dsmmelbas  22007  frlmelbas  22024  frlmphl  22049  islindf4  22106  rnascl  22161  psrlinv  22225  opsrbaslem  22320  evlseu  22354  evlsval3  22360  mpfsubrg  22382  psdmvr  22452  evl1sca  22614  evls1var  22618  matbas  22690  matplusg  22691  matsca  22692  matvsca  22693  matbas2d  22700  matsubgcell  22711  matmulcell  22722  ofco2  22728  mattposm  22736  mat1f1o  22755  mdetunilem8  22896  madugsum  22920  cramerimplem2  22964  decpmatmullem  23051  paste  23574  ptpjcn  23892  uptx  23906  xpstopnlem1  24090  alexsubALTlem4  24331  cnextf  24347  submtmd  24385  ussval  24540  tuslem  24547  psmetge0  24593  xmetge0  24625  setsmsds  24757  sgrim  24912  tnglem  24921  tngtset  24930  tngngp2  24933  resubmet  25083  pcorev2  25311  om1plusg  25317  om1tset  25318  om1opn  25319  pi1grplem  25332  clmadd  25357  clmmul  25358  clmcj  25359  tcphtopn  25509  tchnmfval  25511  bcthlem1  25607  bcthlem2  25608  bcthlem4  25610  bcth3  25614  rrxmval  25688  rrxmfval  25689  rrxdsfi  25694  ehlbase  25698  minveclem3b  25711  pjthlem1  25720  volun  25828  voliun  25837  uniioovol  25862  itg2i1fseq  26038  itgcnlem  26072  iblabslem  26110  limcres  26168  cnplimc  26169  ply1termlem  26483  0dgr  26526  taylthlem1  26664  abelth  26732  lawcos  27108  lgambdd  27328  basellem8  27379  musum  27482  chtub  27503  dchrval  27525  dchrinvcl  27544  lgsval4lem  27599  lgsquadlem2  27672  m1lgs  27679  cuteq0  28135  precsexlem11  28537  seqsval  28608  n0bday  28672  zseo  28742  mirauto  29090  lmiisolem  29235  ttglem  29387  axlowdimlem16  29469  ebtwntg  29494  ecgrtg  29495  elntg2  29497  nbgrval  29851  uvtxupgrres  29923  pthhashvtx  30249  clwlknf1oclwwlknlem3  30608  eucrct2eupth  30780  smcnlem  31233  siii  31389  pjhthlem1  31927  sbcies  33018  imadifxp  33129  dfimafnf  33164  ccatws1f1olast  33449  gsummulsubdishift1  33563  gsumwun  33571  symgcom  33578  cycpmconjslem1  33649  rloc0g  33767  rloc1r  33768  resvlem  33828  qusker  33844  elrspunsn  33913  opprqusplusg  33947  idlsrgbas  33970  idlsrgplusg  33971  idlsrgmulr  33973  idlsrgtset  33974  idlsrgmulrval  33975  fldextrspundgdvdslem  34246  fldextrspundgdvds  34247  irredminply  34282  algextdeglem4  34286  algextdeglem5  34287  constrrtcc  34301  cos9thpinconstrlem1  34355  mdetpmtr12  34391  zarcls  34440  zar0ring  34444  pstmval  34461  xpinpreima2  34473  pnfneige0  34517  zlmds  34528  zlmtset  34529  esumid  34610  esumrnmpt  34618  sxsigon  34759  carsgclctunlem1  34884  circlemethnat  35205  fnrelpredd  35651  filnetlem4  37091  setsstrset  37975  finxpreclem4  38237  itg2addnclem  38509  iblabsnclem  38521  areacirc  38551  fnopabco  38577  heiborlem8  38672  rngoi  38753  drngoi  38805  ldualvsub  40132  dalemrotyz  40635  dalem6  40645  dalem7  40646  dalem11  40651  dalem12  40652  dalemrotps  40668  dalem30  40679  dalem35  40684  cdleme1  41204  cdleme9  41230  cdleme20c  41288  cdleme20d  41289  cdlemefrs29clN  41376  cdleme37m  41439  cdleme43aN  41466  cdlemg1b2  41548  cdlemg4f  41592  cdlemh2  41793  erngdvlem1  41965  erngdvlem2N  41966  erngdvlem3  41967  erngdvlem4  41968  erngdvlem1-rN  41973  erngdvlem2-rN  41974  erngdvlem3-rN  41975  erngdvlem4-rN  41976  dvh4dimN  42424  lcdvsub  42594  hlhilsca  42912  hlhilbase  42913  hlhilplus  42914  hlhilvsca  42924  hlhilip  42925  hlhilipval  42926  25or6to4  43176  reelznn0nn  43453  rnasclg  43491  prjspeclsp  43562  mzpcompact2lem  43700  eldioph2lem1  43709  fiphp3d  43764  rmxypairf1o  43856  wopprc  43975  lmhmlnmsplit  44032  rp-tfslim  44298  onsucunitp  44318  clcnvlem  44567  mnringnmulrd  45156  mnringbaserd  45158  mnringmulrd  45165  dmmptdff  46157  dmmptdf2  46166  ellimcabssub0  46551  cosknegpi  46801  dvnprodlem1  46878  fourierdlem58  47096  fourierdlem59  47097  fourierdlem72  47110  fourierdlem80  47118  sqwvfourb  47161  etransclem28  47194  etransclem41  47207  omef  47428  dfaimafn  48157  afv2co2  48249  sbgoldbo  48807  rrxlinesc  49769  rrxlinec  49770  rrx2linest2  49778  rrxsphere  49782  itsclinecirc0b  49808  itsclquadb  49810  2oppf  50162  idfullsubc  50191  oppc1stf  50318  oppc2ndf  50319  dfinito4  50531  prstcnid  50583  prstcthin  50591