Theorem eqtr4id 2796

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  rabeqcda  3448  iftrue  4531  iffalse  4534  difprsn1  4800  dmmptg  6262  setlikespec  6346  funimacnv  6647  dmmptd  6713  resasplit  6778  dffv3  6902  dfimafn  6971  fniinfv  6987  dffv2  7004  fvco2  7006  fniunfv  7267  isoini  7358  fvmpopr2d  7595  zfrep6  7979  oprabco  8121  suppco  8231  oeeulem  8639  ixpconstg  8946  sbthlem4  9126  sbthlem5  9127  sbthlem6  9128  supval2  9495  hartogslem1  9582  cantnflem1d  9728  alephsuc2  10120  dfac3  10161  hsmexlem5  10470  axdc2lem  10488  gruima  10842  eqneg  11987  zeo  12704  fseq1p1m1  13638  hashfzo  14468  hashimarn  14479  wrdval  14555  wrdnval  14583  repswswrd  14822  s1co  14872  swrds2  14979  s7f1o  15005  modfsummod  15830  telfsumo  15838  mulgcd  16585  algcvg  16613  phiprmpw  16813  phisum  16828  strfv3  17241  resseqnbas  17287  resslemOLD  17288  pwssnf1o  17543  imassca  17564  homfeq  17737  oppcbas  17761  resscatc  18154  estrcbasbas  18175  funcestrcsetclem7  18191  funcestrcsetclem8  18192  funcestrcsetclem9  18193  fthestrcsetc  18195  fullestrcsetc  18196  equivestrcsetc  18197  setc1strwun  18198  funcsetcestrclem7  18206  funcsetcestrclem8  18207  funcsetcestrclem9  18208  fthsetcestrc  18210  fullsetcestrc  18211  lubsn  18527  ipotset  18578  ipole  18579  plusfeq  18661  pws0g  18786  frmd0  18873  efmndtset  18892  oppgplusfval  19366  gsmsymgrfix  19446  gsmsymgreq  19450  psgnunilem2  19513  sylow3lem2  19646  oppglsm  19660  frgpuplem  19790  frgpupf  19791  frgpup1  19793  frgpup3lem  19795  gsumzoppg  19962  ablfac1eu  20093  pgpfaclem1  20101  pwsmgp  20324  opprmulfval  20336  rdivmuldivd  20413  dfrhm2  20474  subrg1  20582  staffn  20844  issrngd  20856  scafeq  20880  lbsextlem4  21163  sralem  21175  sralemOLD  21176  sravsca  21185  sravscaOLD  21186  sraip  21187  2idlbas  21273  zlmlem  21527  zlmlemOLD  21528  zlmvsca  21536  znbaslem  21553  znbaslemOLD  21554  ipfeq  21668  ssipeq  21674  thlbas  21714  thlbasOLD  21715  thlle  21716  thlleOLD  21717  thloc  21719  dsmmbase  21755  dsmmelbas  21759  frlmelbas  21776  frlmphl  21801  islindf4  21858  rnascl  21911  psrlinv  21975  opsrbaslem  22067  opsrbaslemOLD  22068  evlseu  22107  mpfsubrg  22127  psdmvr  22173  ply1scl0OLD  22294  evl1sca  22338  evls1var  22342  matbas  22417  matplusg  22418  matsca  22419  matscaOLD  22420  matvsca  22421  matvscaOLD  22422  matbas2d  22429  matsubgcell  22440  matmulcell  22451  ofco2  22457  mattposm  22465  mat1f1o  22484  mdetunilem8  22625  madugsum  22649  cramerimplem2  22690  decpmatmullem  22777  paste  23302  ptpjcn  23619  uptx  23633  xpstopnlem1  23817  alexsubALTlem4  24058  cnextf  24074  submtmd  24112  ussval  24268  tuslem  24275  tuslemOLD  24276  psmetge0  24322  xmetge0  24354  setsmsds  24487  setsmsdsOLD  24488  sgrim  24644  tnglem  24653  tnglemOLD  24654  tngtset  24670  tngngp2  24673  resubmet  24823  pcorev2  25061  om1plusg  25067  om1tset  25068  om1opn  25069  pi1grplem  25082  clmadd  25107  clmmul  25108  clmcj  25109  tcphtopn  25260  tchnmfval  25262  bcthlem1  25358  bcthlem2  25359  bcthlem4  25361  bcth3  25365  rrxmval  25439  rrxmfval  25440  rrxdsfi  25445  ehlbase  25449  minveclem3b  25462  pjthlem1  25471  volun  25580  voliun  25589  uniioovol  25614  itg2i1fseq  25790  itgcnlem  25825  iblabslem  25863  limcres  25921  cnplimc  25922  ply1termlem  26242  0dgr  26284  taylthlem1  26415  abelth  26485  lawcos  26859  lgambdd  27080  basellem8  27131  musum  27234  chtub  27256  dchrval  27278  dchrinvcl  27297  lgsval4lem  27352  lgsquadlem2  27425  m1lgs  27432  cuteq0  27877  precsexlem11  28241  seqsval  28294  n0sbday  28354  zseo  28406  mirauto  28692  lmiisolem  28804  ttglem  28885  ttglemOLD  28886  axlowdimlem16  28972  ebtwntg  28997  ecgrtg  28998  elntg2  29000  nbgrval  29353  uvtxupgrres  29425  clwlknf1oclwwlknlem3  30102  eucrct2eupth  30264  smcnlem  30716  siii  30872  pjhthlem1  31410  sbcies  32507  imadifxp  32614  dfimafnf  32646  funcnvmpt  32677  ccatws1f1olast  32937  gsumwun  33068  symgcom  33103  cycpmconjslem1  33174  rloc0g  33275  rloc1r  33276  resvlem  33357  resvlemOLD  33358  qusker  33377  elrspunsn  33457  opprqusplusg  33517  idlsrgbas  33532  idlsrgplusg  33533  idlsrgmulr  33535  idlsrgtset  33536  idlsrgmulrval  33537  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  irredminply  33757  algextdeglem4  33761  algextdeglem5  33762  constrrtcc  33776  mdetpmtr12  33824  zarcls  33873  zar0ring  33877  pstmval  33894  xpinpreima2  33906  pnfneige0  33950  zlmds  33961  zlmdsOLD  33962  zlmtset  33963  zlmtsetOLD  33964  esumid  34045  esumrnmpt  34053  sxsigon  34193  carsgclctunlem1  34319  circlemethnat  34656  fnrelpredd  35103  f1resfz0f1d  35119  pthhashvtx  35133  filnetlem4  36382  setsstrset  37137  finxpreclem4  37395  itg2addnclem  37678  iblabsnclem  37690  areacirc  37720  fnopabco  37730  heiborlem8  37825  rngoi  37906  drngoi  37958  ldualvsub  39156  dalemrotyz  39660  dalem6  39670  dalem7  39671  dalem11  39676  dalem12  39677  dalemrotps  39693  dalem30  39704  dalem35  39709  cdleme1  40229  cdleme9  40255  cdleme20c  40313  cdleme20d  40314  cdlemefrs29clN  40401  cdleme37m  40464  cdleme43aN  40491  cdlemg1b2  40573  cdlemg4f  40617  cdlemh2  40818  erngdvlem1  40990  erngdvlem2N  40991  erngdvlem3  40992  erngdvlem4  40993  erngdvlem1-rN  40998  erngdvlem2-rN  40999  erngdvlem3-rN  41000  erngdvlem4-rN  41001  dvh4dimN  41449  lcdvsub  41619  hlhilsca  41937  hlhilbase  41938  hlhilplus  41939  hlhilvsca  41953  hlhilip  41954  hlhilipval  41955  reelznn0nn  42479  rnasclg  42509  evlsval3  42569  prjspeclsp  42622  mzpcompact2lem  42762  eldioph2lem1  42771  fiphp3d  42830  rmxypairf1o  42923  wopprc  43042  lmhmlnmsplit  43099  rp-tfslim  43366  onsucunitp  43386  clcnvlem  43636  mnringnmulrd  44228  mnringnmulrdOLD  44229  mnringbaserd  44232  mnringmulrd  44240  dmmptdff  45228  dmmptdf2  45238  ellimcabssub0  45632  cosknegpi  45884  dvnprodlem1  45961  fourierdlem58  46179  fourierdlem59  46180  fourierdlem72  46193  fourierdlem80  46201  sqwvfourb  46244  etransclem28  46277  etransclem41  46290  omef  46511  dfaimafn  47177  afv2co2  47269  sbgoldbo  47774  rrxlinesc  48656  rrxlinec  48657  rrx2linest2  48665  rrxsphere  48669  itsclinecirc0b  48695  itsclquadb  48697  prstcnid  49155  prstcthin  49165