Theorem eqtr4id 2810

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

Syntax hints:   → wi 4   = wceq 1554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-cleq 2748

This theorem is referenced by:  rabeqcda  3419  iftrue  4480  iffalse  4483  difprsn1  4754  csbcnv  5851  dmmptg  6218  setlikespec  6301  funimacnv  6591  dmmptd  6655  resasplit  6723  dffv3  6852  dfimafn  6918  fniinfv  6934  dffv2  6951  fvco2  6953  funcnvmpt  6966  fniunfv  7220  isoini  7311  fvmpopr2d  7547  zfrep6OLD  7925  oprabco  8063  suppco  8174  oeeulem  8559  ixpconstg  8877  sbthlem4  9051  sbthlem5  9052  sbthlem6  9053  supval2  9391  hartogslem1  9480  cantnflem1d  9633  alephsuc2  10026  dfac3  10067  hsmexlem5  10377  axdc2lem  10395  gruima  10750  eqneg  11901  zeo  12649  fseq1p1m1  13593  hashfzo  14432  hashimarn  14443  wrdval  14519  wrdnval  14548  repswswrd  14787  s1co  14836  swrds2  14943  s7f1o  14969  modfsummod  15798  telfsumo  15806  indsumhash  15833  mulgcd  16558  algcvg  16586  phiprmpw  16787  phisum  16802  strfv3  17216  resseqnbas  17254  pwssnf1o  17504  imassca  17525  homfeq  17702  oppcbas  17726  resscatc  18118  estrcbasbas  18139  funcestrcsetclem7  18154  funcestrcsetclem8  18155  funcestrcsetclem9  18156  fthestrcsetc  18158  fullestrcsetc  18159  equivestrcsetc  18160  setc1strwun  18161  funcsetcestrclem7  18169  funcsetcestrclem8  18170  funcsetcestrclem9  18171  fthsetcestrc  18173  fullsetcestrc  18174  lubsn  18490  ipotset  18541  ipole  18542  plusfeq  18658  pws0g  18783  frmd0  18870  efmndtset  18889  oppgplusfval  19364  gsmsymgrfix  19444  gsmsymgreq  19448  psgnunilem2  19511  sylow3lem2  19644  oppglsm  19658  frgpuplem  19788  frgpupf  19789  frgpup1  19791  frgpup3lem  19793  gsumzoppg  19960  ablfac1eu  20091  pgpfaclem1  20099  pwsmgp  20347  opprmulfval  20360  rdivmuldivd  20434  dfrhm2  20495  subrg1  20604  staffn  20865  issrngd  20877  scafeq  20922  lbsextlem4  21204  sralem  21216  sravsca  21221  sraip  21222  2idlbas  21306  zlmlem  21541  zlmvsca  21546  znbaslem  21563  ipfeq  21675  ssipeq  21681  thlbas  21721  thlle  21722  thloc  21724  dsmmbase  21760  dsmmelbas  21764  frlmelbas  21781  frlmphl  21806  islindf4  21863  rnascl  21916  psrlinv  21980  opsrbaslem  22075  evlseu  22109  evlsval3  22115  mpfsubrg  22137  psdmvr  22207  evl1sca  22370  evls1var  22374  matbas  22446  matplusg  22447  matsca  22448  matvsca  22449  matbas2d  22456  matsubgcell  22467  matmulcell  22478  ofco2  22484  mattposm  22492  mat1f1o  22511  mdetunilem8  22652  madugsum  22676  cramerimplem2  22717  decpmatmullem  22804  paste  23327  ptpjcn  23644  uptx  23658  xpstopnlem1  23842  alexsubALTlem4  24083  cnextf  24099  submtmd  24137  ussval  24292  tuslem  24299  psmetge0  24345  xmetge0  24377  setsmsds  24509  sgrim  24664  tnglem  24673  tngtset  24682  tngngp2  24685  resubmet  24835  pcorev2  25063  om1plusg  25069  om1tset  25070  om1opn  25071  pi1grplem  25084  clmadd  25109  clmmul  25110  clmcj  25111  tcphtopn  25261  tchnmfval  25263  bcthlem1  25359  bcthlem2  25360  bcthlem4  25362  bcth3  25366  rrxmval  25440  rrxmfval  25441  rrxdsfi  25446  ehlbase  25450  minveclem3b  25463  pjthlem1  25472  volun  25580  voliun  25589  uniioovol  25614  itg2i1fseq  25790  itgcnlem  25825  iblabslem  25863  limcres  25921  cnplimc  25922  ply1termlem  26236  0dgr  26278  taylthlem1  26406  abelth  26474  lawcos  26851  lgambdd  27071  basellem8  27122  musum  27225  chtub  27246  dchrval  27268  dchrinvcl  27287  lgsval4lem  27342  lgsquadlem2  27415  m1lgs  27422  cuteq0  27878  precsexlem11  28280  seqsval  28351  n0bday  28415  zseo  28485  mirauto  28823  lmiisolem  28935  ttglem  29015  axlowdimlem16  29097  ebtwntg  29122  ecgrtg  29123  elntg2  29125  nbgrval  29476  uvtxupgrres  29548  clwlknf1oclwwlknlem3  30224  eucrct2eupth  30386  smcnlem  30839  siii  30995  pjhthlem1  31533  sbcies  32628  imadifxp  32743  dfimafnf  32781  ccatws1f1olast  33084  gsummulsubdishift1  33202  gsumwun  33210  symgcom  33217  cycpmconjslem1  33288  rloc0g  33407  rloc1r  33408  resvlem  33473  qusker  33489  elrspunsn  33569  opprqusplusg  33631  idlsrgbas  33654  idlsrgplusg  33655  idlsrgmulr  33657  idlsrgtset  33658  idlsrgmulrval  33659  fldextrspundgdvdslem  33931  fldextrspundgdvds  33932  irredminply  33967  algextdeglem4  33971  algextdeglem5  33972  constrrtcc  33986  cos9thpinconstrlem1  34040  mdetpmtr12  34076  zarcls  34125  zar0ring  34129  pstmval  34146  xpinpreima2  34158  pnfneige0  34202  zlmds  34213  zlmtset  34214  esumid  34295  esumrnmpt  34303  sxsigon  34443  carsgclctunlem1  34568  circlemethnat  34892  fnrelpredd  35342  f1resfz0f1d  35412  pthhashvtx  35426  filnetlem4  36689  setsstrset  37574  finxpreclem4  37836  itg2addnclem  38118  iblabsnclem  38130  areacirc  38160  fnopabco  38170  heiborlem8  38265  rngoi  38346  drngoi  38398  ldualvsub  39727  dalemrotyz  40230  dalem6  40240  dalem7  40241  dalem11  40246  dalem12  40247  dalemrotps  40263  dalem30  40274  dalem35  40279  cdleme1  40799  cdleme9  40825  cdleme20c  40883  cdleme20d  40884  cdlemefrs29clN  40971  cdleme37m  41034  cdleme43aN  41061  cdlemg1b2  41143  cdlemg4f  41187  cdlemh2  41388  erngdvlem1  41560  erngdvlem2N  41561  erngdvlem3  41562  erngdvlem4  41563  erngdvlem1-rN  41568  erngdvlem2-rN  41569  erngdvlem3-rN  41570  erngdvlem4-rN  41571  dvh4dimN  42019  lcdvsub  42189  hlhilsca  42507  hlhilbase  42508  hlhilplus  42509  hlhilvsca  42519  hlhilip  42520  hlhilipval  42521  reelznn0nn  43031  rnasclg  43069  prjspeclsp  43142  mzpcompact2lem  43280  eldioph2lem1  43289  fiphp3d  43344  rmxypairf1o  43436  wopprc  43555  lmhmlnmsplit  43612  rp-tfslim  43878  onsucunitp  43898  clcnvlem  44147  mnringnmulrd  44738  mnringbaserd  44740  mnringmulrd  44747  dmmptdff  45747  dmmptdf2  45756  ellimcabssub0  46141  cosknegpi  46391  dvnprodlem1  46468  fourierdlem58  46686  fourierdlem59  46687  fourierdlem72  46700  fourierdlem80  46708  sqwvfourb  46751  etransclem28  46784  etransclem41  46797  omef  47018  dfaimafn  47707  afv2co2  47799  sbgoldbo  48357  rrxlinesc  49305  rrxlinec  49306  rrx2linest2  49314  rrxsphere  49318  itsclinecirc0b  49344  itsclquadb  49346  2oppf  49701  idfullsubc  49730  oppc1stf  49857  oppc2ndf  49858  dfinito4  50070  prstcnid  50122  prstcthin  50130