Theorem eqtr4id 2791

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  rabeqcda  3401  iftrue  4473  iffalse  4476  difprsn1  4744  dmmptg  6198  setlikespec  6281  funimacnv  6571  dmmptd  6635  resasplit  6702  dffv3  6828  dfimafn  6894  fniinfv  6910  dffv2  6927  fvco2  6929  funcnvmpt  6941  fniunfv  7193  isoini  7284  fvmpopr2d  7520  zfrep6OLD  7899  oprabco  8037  suppco  8147  oeeulem  8528  ixpconstg  8845  sbthlem4  9019  sbthlem5  9020  sbthlem6  9021  supval2  9359  hartogslem1  9448  cantnflem1d  9598  alephsuc2  9991  dfac3  10032  hsmexlem5  10341  axdc2lem  10359  gruima  10714  eqneg  11864  zeo  12604  fseq1p1m1  13541  hashfzo  14380  hashimarn  14391  wrdval  14467  wrdnval  14496  repswswrd  14735  s1co  14784  swrds2  14891  s7f1o  14917  modfsummod  15746  telfsumo  15754  indsumhash  15781  mulgcd  16506  algcvg  16534  phiprmpw  16735  phisum  16750  strfv3  17163  resseqnbas  17201  pwssnf1o  17451  imassca  17472  homfeq  17649  oppcbas  17673  resscatc  18065  estrcbasbas  18086  funcestrcsetclem7  18101  funcestrcsetclem8  18102  funcestrcsetclem9  18103  fthestrcsetc  18105  fullestrcsetc  18106  equivestrcsetc  18107  setc1strwun  18108  funcsetcestrclem7  18116  funcsetcestrclem8  18117  funcsetcestrclem9  18118  fthsetcestrc  18120  fullsetcestrc  18121  lubsn  18437  ipotset  18488  ipole  18489  plusfeq  18605  pws0g  18730  frmd0  18817  efmndtset  18836  oppgplusfval  19312  gsmsymgrfix  19392  gsmsymgreq  19396  psgnunilem2  19459  sylow3lem2  19592  oppglsm  19606  frgpuplem  19736  frgpupf  19737  frgpup1  19739  frgpup3lem  19741  gsumzoppg  19908  ablfac1eu  20039  pgpfaclem1  20047  pwsmgp  20295  opprmulfval  20308  rdivmuldivd  20382  dfrhm2  20443  subrg1  20548  staffn  20809  issrngd  20821  scafeq  20866  lbsextlem4  21149  sralem  21161  sravsca  21166  sraip  21167  2idlbas  21251  zlmlem  21504  zlmvsca  21509  znbaslem  21526  ipfeq  21638  ssipeq  21644  thlbas  21684  thlle  21685  thloc  21687  dsmmbase  21723  dsmmelbas  21727  frlmelbas  21744  frlmphl  21769  islindf4  21826  rnascl  21879  psrlinv  21943  opsrbaslem  22036  evlseu  22070  evlsval3  22076  mpfsubrg  22098  psdmvr  22144  evl1sca  22308  evls1var  22312  matbas  22387  matplusg  22388  matsca  22389  matvsca  22390  matbas2d  22397  matsubgcell  22408  matmulcell  22419  ofco2  22425  mattposm  22433  mat1f1o  22452  mdetunilem8  22593  madugsum  22617  cramerimplem2  22658  decpmatmullem  22745  paste  23268  ptpjcn  23585  uptx  23599  xpstopnlem1  23783  alexsubALTlem4  24024  cnextf  24040  submtmd  24078  ussval  24233  tuslem  24240  psmetge0  24286  xmetge0  24318  setsmsds  24450  sgrim  24605  tnglem  24614  tngtset  24623  tngngp2  24626  resubmet  24776  pcorev2  25004  om1plusg  25010  om1tset  25011  om1opn  25012  pi1grplem  25025  clmadd  25050  clmmul  25051  clmcj  25052  tcphtopn  25202  tchnmfval  25204  bcthlem1  25300  bcthlem2  25301  bcthlem4  25303  bcth3  25307  rrxmval  25381  rrxmfval  25382  rrxdsfi  25387  ehlbase  25391  minveclem3b  25404  pjthlem1  25413  volun  25521  voliun  25530  uniioovol  25555  itg2i1fseq  25731  itgcnlem  25766  iblabslem  25804  limcres  25862  cnplimc  25863  ply1termlem  26180  0dgr  26222  taylthlem1  26352  abelth  26422  lawcos  26797  lgambdd  27018  basellem8  27069  musum  27172  chtub  27194  dchrval  27216  dchrinvcl  27235  lgsval4lem  27290  lgsquadlem2  27363  m1lgs  27370  cuteq0  27826  precsexlem11  28228  seqsval  28299  n0bday  28363  zseo  28433  mirauto  28771  lmiisolem  28883  ttglem  28963  axlowdimlem16  29045  ebtwntg  29070  ecgrtg  29071  elntg2  29073  nbgrval  29424  uvtxupgrres  29496  clwlknf1oclwwlknlem3  30173  eucrct2eupth  30335  smcnlem  30788  siii  30944  pjhthlem1  31482  sbcies  32577  imadifxp  32691  dfimafnf  32729  ccatws1f1olast  33032  gsummulsubdishift1  33149  gsumwun  33157  symgcom  33164  cycpmconjslem1  33235  rloc0g  33352  rloc1r  33353  resvlem  33413  qusker  33429  elrspunsn  33509  opprqusplusg  33569  idlsrgbas  33584  idlsrgplusg  33585  idlsrgmulr  33587  idlsrgtset  33588  idlsrgmulrval  33589  fldextrspundgdvdslem  33845  fldextrspundgdvds  33846  irredminply  33881  algextdeglem4  33885  algextdeglem5  33886  constrrtcc  33900  cos9thpinconstrlem1  33954  mdetpmtr12  33990  zarcls  34039  zar0ring  34043  pstmval  34060  xpinpreima2  34072  pnfneige0  34116  zlmds  34127  zlmtset  34128  esumid  34209  esumrnmpt  34217  sxsigon  34357  carsgclctunlem1  34482  circlemethnat  34806  fnrelpredd  35255  f1resfz0f1d  35317  pthhashvtx  35331  filnetlem4  36584  setsstrset  37461  finxpreclem4  37721  itg2addnclem  38003  iblabsnclem  38015  areacirc  38045  fnopabco  38055  heiborlem8  38150  rngoi  38231  drngoi  38283  ldualvsub  39612  dalemrotyz  40115  dalem6  40125  dalem7  40126  dalem11  40131  dalem12  40132  dalemrotps  40148  dalem30  40159  dalem35  40164  cdleme1  40684  cdleme9  40710  cdleme20c  40768  cdleme20d  40769  cdlemefrs29clN  40856  cdleme37m  40919  cdleme43aN  40946  cdlemg1b2  41028  cdlemg4f  41072  cdlemh2  41273  erngdvlem1  41445  erngdvlem2N  41446  erngdvlem3  41447  erngdvlem4  41448  erngdvlem1-rN  41453  erngdvlem2-rN  41454  erngdvlem3-rN  41455  erngdvlem4-rN  41456  dvh4dimN  41904  lcdvsub  42074  hlhilsca  42392  hlhilbase  42393  hlhilplus  42394  hlhilvsca  42404  hlhilip  42405  hlhilipval  42406  reelznn0nn  42917  rnasclg  42955  prjspeclsp  43056  mzpcompact2lem  43194  eldioph2lem1  43203  fiphp3d  43262  rmxypairf1o  43354  wopprc  43473  lmhmlnmsplit  43530  rp-tfslim  43796  onsucunitp  43816  clcnvlem  44065  mnringnmulrd  44656  mnringbaserd  44658  mnringmulrd  44665  dmmptdff  45667  dmmptdf2  45677  ellimcabssub0  46062  cosknegpi  46312  dvnprodlem1  46389  fourierdlem58  46607  fourierdlem59  46608  fourierdlem72  46621  fourierdlem80  46629  sqwvfourb  46672  etransclem28  46705  etransclem41  46718  omef  46939  dfaimafn  47610  afv2co2  47702  sbgoldbo  48260  rrxlinesc  49208  rrxlinec  49209  rrx2linest2  49217  rrxsphere  49221  itsclinecirc0b  49247  itsclquadb  49249  2oppf  49604  idfullsubc  49633  oppc1stf  49760  oppc2ndf  49761  dfinito4  49973  prstcnid  50025  prstcthin  50033