Theorem eqtr4id 2798

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  iftrue  4462  iffalse  4465  difprsn1  4730  dmmptg  6134  setlikespec  6217  funimacnv  6499  dmmptd  6562  resasplit  6628  dffv3  6752  dfimafn  6814  fniinfv  6828  dffv2  6845  fvco2  6847  fniunfv  7102  isoini  7189  fvmpopr2d  7412  zfrep6  7771  oprabco  7907  suppco  7993  oeeulem  8394  ixpconstg  8652  sbthlem4  8826  sbthlem5  8827  sbthlem6  8828  supval2  9144  hartogslem1  9231  cantnflem1d  9376  alephsuc2  9767  dfac3  9808  hsmexlem5  10117  axdc2lem  10135  gruima  10489  eqneg  11625  zeo  12336  fseq1p1m1  13259  hashfzo  14072  hashimarn  14083  wrdval  14148  wrdnval  14176  repswswrd  14425  s1co  14474  swrds2  14581  modfsummod  15434  telfsumo  15442  mulgcd  16184  algcvg  16209  phiprmpw  16405  phisum  16419  strfv3  16834  resseqnbas  16877  resslemOLD  16878  pwssnf1o  17126  imassca  17147  homfeq  17320  oppcbas  17345  oppcbasOLD  17346  resscatc  17740  estrcbasbas  17763  funcestrcsetclem7  17779  funcestrcsetclem8  17780  funcestrcsetclem9  17781  fthestrcsetc  17783  fullestrcsetc  17784  equivestrcsetc  17785  setc1strwun  17786  funcsetcestrclem7  17794  funcsetcestrclem8  17795  funcsetcestrclem9  17796  fthsetcestrc  17798  fullsetcestrc  17799  lubsn  18115  ipotset  18166  ipole  18167  plusfeq  18249  pws0g  18336  frmd0  18414  efmndtset  18433  oppgplusfval  18867  gsmsymgrfix  18951  gsmsymgreq  18955  psgnunilem2  19018  sylow3lem2  19148  oppglsm  19162  frgpuplem  19293  frgpupf  19294  frgpup1  19296  frgpup3lem  19298  gsumzoppg  19460  ablfac1eu  19591  pgpfaclem1  19599  pwsmgp  19772  opprmulfval  19779  dfrhm2  19876  subrg1  19949  staffn  20024  issrngd  20036  scafeq  20058  lbsextlem4  20338  sralem  20354  sralemOLD  20355  sravsca  20363  sraip  20364  zlmlem  20630  zlmlemOLD  20631  zlmvsca  20639  znbaslem  20654  znbaslemOLD  20655  ipfeq  20767  ssipeq  20773  thlbas  20813  thlle  20814  thloc  20816  dsmmbase  20852  dsmmelbas  20856  frlmelbas  20873  frlmphl  20898  islindf4  20955  rnascl  21005  psrlinv  21076  opsrbaslem  21160  opsrbaslemOLD  21161  evlseu  21203  mpfsubrg  21223  ply1scl0  21371  evl1sca  21410  evls1var  21414  matbas  21470  matplusg  21471  matsca  21472  matvsca  21473  matbas2d  21480  matsubgcell  21491  matmulcell  21502  ofco2  21508  mattposm  21516  mat1f1o  21535  mdetunilem8  21676  madugsum  21700  cramerimplem2  21741  decpmatmullem  21828  paste  22353  ptpjcn  22670  uptx  22684  xpstopnlem1  22868  alexsubALTlem4  23109  cnextf  23125  submtmd  23163  ussval  23319  tuslem  23326  tuslemOLD  23327  psmetge0  23373  xmetge0  23405  setsmsds  23537  sgrim  23693  tnglem  23702  tnglemOLD  23703  tngtset  23719  tngngp2  23722  resubmet  23871  pcorev2  24097  om1plusg  24103  om1tset  24104  om1opn  24105  pi1grplem  24118  clmadd  24143  clmmul  24144  clmcj  24145  tcphtopn  24295  tchnmfval  24297  bcthlem1  24393  bcthlem2  24394  bcthlem4  24396  bcth3  24400  rrxmval  24474  rrxmfval  24475  rrxdsfi  24480  ehlbase  24484  minveclem3b  24497  pjthlem1  24506  volun  24614  voliun  24623  uniioovol  24648  itg2i1fseq  24825  itgcnlem  24859  iblabslem  24897  limcres  24955  cnplimc  24956  ply1termlem  25269  0dgr  25311  taylthlem1  25437  abelth  25505  lawcos  25871  lgambdd  26091  basellem8  26142  musum  26245  chtub  26265  dchrval  26287  dchrinvcl  26306  lgsval4lem  26361  lgsquadlem2  26434  m1lgs  26441  mirauto  26949  lmiisolem  27061  ttglem  27141  ttglemOLD  27142  axlowdimlem16  27228  ebtwntg  27253  ecgrtg  27254  elntg2  27256  nbgrval  27606  uvtxupgrres  27678  clwlknf1oclwwlknlem3  28348  eucrct2eupth  28510  smcnlem  28960  siii  29116  pjhthlem1  29654  sbcies  30737  imadifxp  30841  dfimafnf  30872  funcnvmpt  30906  symgcom  31254  cycpmconjslem1  31323  rdivmuldivd  31390  resvlem  31432  resvlemOLD  31433  qusker  31451  idlsrgbas  31551  idlsrgplusg  31552  idlsrgmulr  31554  idlsrgtset  31555  idlsrgmulrval  31556  mdetpmtr12  31677  zarcls  31726  zar0ring  31730  pstmval  31747  xpinpreima2  31759  pnfneige0  31803  zlmds  31814  zlmtset  31815  esumid  31912  esumrnmpt  31920  sxsigon  32060  carsgclctunlem1  32184  circlemethnat  32521  fnrelpredd  32961  f1resfz0f1d  32972  pthhashvtx  32989  filnetlem4  34497  setsstrset  35234  finxpreclem4  35492  itg2addnclem  35755  iblabsnclem  35767  areacirc  35797  fnopabco  35808  heiborlem8  35903  rngoi  35984  drngoi  36036  ldualvsub  37096  dalemrotyz  37599  dalem6  37609  dalem7  37610  dalem11  37615  dalem12  37616  dalemrotps  37632  dalem30  37643  dalem35  37648  cdleme1  38168  cdleme9  38194  cdleme20c  38252  cdleme20d  38253  cdlemefrs29clN  38340  cdleme37m  38403  cdleme43aN  38430  cdlemg1b2  38512  cdlemg4f  38556  cdlemh2  38757  erngdvlem1  38929  erngdvlem2N  38930  erngdvlem3  38931  erngdvlem4  38932  erngdvlem1-rN  38937  erngdvlem2-rN  38938  erngdvlem3-rN  38939  erngdvlem4-rN  38940  dvh4dimN  39388  lcdvsub  39558  hlhilsca  39876  hlhilbase  39877  hlhilplus  39878  hlhilvsca  39892  hlhilip  39893  hlhilipval  39894  rnasclg  40149  evlsval3  40195  evlsbagval  40198  prjspeclsp  40372  mzpcompact2lem  40489  eldioph2lem1  40498  fiphp3d  40557  rmxypairf1o  40649  wopprc  40768  lmhmlnmsplit  40828  clcnvlem  41120  mnringnmulrd  41716  mnringnmulrdOLD  41717  mnringbaserd  41720  mnringmulrd  41728  dmmptdf  42652  dmmptdf2  42665  ellimcabssub0  43048  cosknegpi  43300  fourierdlem58  43595  fourierdlem59  43596  fourierdlem72  43609  fourierdlem80  43617  sqwvfourb  43660  etransclem28  43693  etransclem41  43706  omef  43924  dfaimafn  44544  afv2co2  44636  sbgoldbo  45127  rrxlinesc  45969  rrxlinec  45970  rrx2linest2  45978  rrxsphere  45982  itsclinecirc0b  46008  itsclquadb  46010  prstcnid  46235  prstcthin  46243