Theorem eqtr4id 2784

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722

This theorem is referenced by:  rabeqcda  3404  iftrue  4479  iffalse  4482  difprsn1  4750  dmmptg  6186  setlikespec  6268  funimacnv  6558  dmmptd  6622  resasplit  6689  dffv3  6813  dfimafn  6879  fniinfv  6895  dffv2  6912  fvco2  6914  fniunfv  7176  isoini  7267  fvmpopr2d  7503  zfrep6  7882  oprabco  8021  suppco  8131  oeeulem  8511  ixpconstg  8825  sbthlem4  8998  sbthlem5  8999  sbthlem6  9000  supval2  9334  hartogslem1  9423  cantnflem1d  9573  alephsuc2  9963  dfac3  10004  hsmexlem5  10313  axdc2lem  10331  gruima  10685  eqneg  11833  zeo  12551  fseq1p1m1  13490  hashfzo  14328  hashimarn  14339  wrdval  14415  wrdnval  14444  repswswrd  14683  s1co  14732  swrds2  14839  s7f1o  14865  modfsummod  15693  telfsumo  15701  mulgcd  16451  algcvg  16479  phiprmpw  16679  phisum  16694  strfv3  17107  resseqnbas  17145  pwssnf1o  17394  imassca  17415  homfeq  17592  oppcbas  17616  resscatc  18008  estrcbasbas  18029  funcestrcsetclem7  18044  funcestrcsetclem8  18045  funcestrcsetclem9  18046  fthestrcsetc  18048  fullestrcsetc  18049  equivestrcsetc  18050  setc1strwun  18051  funcsetcestrclem7  18059  funcsetcestrclem8  18060  funcsetcestrclem9  18061  fthsetcestrc  18063  fullsetcestrc  18064  lubsn  18380  ipotset  18431  ipole  18432  plusfeq  18548  pws0g  18673  frmd0  18760  efmndtset  18779  oppgplusfval  19253  gsmsymgrfix  19333  gsmsymgreq  19337  psgnunilem2  19400  sylow3lem2  19533  oppglsm  19547  frgpuplem  19677  frgpupf  19678  frgpup1  19680  frgpup3lem  19682  gsumzoppg  19849  ablfac1eu  19980  pgpfaclem1  19988  pwsmgp  20238  opprmulfval  20250  rdivmuldivd  20324  dfrhm2  20385  subrg1  20490  staffn  20751  issrngd  20763  scafeq  20808  lbsextlem4  21091  sralem  21103  sravsca  21108  sraip  21109  2idlbas  21193  zlmlem  21446  zlmvsca  21451  znbaslem  21468  ipfeq  21580  ssipeq  21586  thlbas  21626  thlle  21627  thloc  21629  dsmmbase  21665  dsmmelbas  21669  frlmelbas  21686  frlmphl  21711  islindf4  21768  rnascl  21821  psrlinv  21885  opsrbaslem  21977  evlseu  22011  mpfsubrg  22031  psdmvr  22077  ply1scl0OLD  22198  evl1sca  22242  evls1var  22246  matbas  22321  matplusg  22322  matsca  22323  matvsca  22324  matbas2d  22331  matsubgcell  22342  matmulcell  22353  ofco2  22359  mattposm  22367  mat1f1o  22386  mdetunilem8  22527  madugsum  22551  cramerimplem2  22592  decpmatmullem  22679  paste  23202  ptpjcn  23519  uptx  23533  xpstopnlem1  23717  alexsubALTlem4  23958  cnextf  23974  submtmd  24012  ussval  24167  tuslem  24174  psmetge0  24220  xmetge0  24252  setsmsds  24384  sgrim  24539  tnglem  24548  tngtset  24557  tngngp2  24560  resubmet  24710  pcorev2  24948  om1plusg  24954  om1tset  24955  om1opn  24956  pi1grplem  24969  clmadd  24994  clmmul  24995  clmcj  24996  tcphtopn  25146  tchnmfval  25148  bcthlem1  25244  bcthlem2  25245  bcthlem4  25247  bcth3  25251  rrxmval  25325  rrxmfval  25326  rrxdsfi  25331  ehlbase  25335  minveclem3b  25348  pjthlem1  25357  volun  25466  voliun  25475  uniioovol  25500  itg2i1fseq  25676  itgcnlem  25711  iblabslem  25749  limcres  25807  cnplimc  25808  ply1termlem  26128  0dgr  26170  taylthlem1  26301  abelth  26371  lawcos  26746  lgambdd  26967  basellem8  27018  musum  27121  chtub  27143  dchrval  27165  dchrinvcl  27184  lgsval4lem  27239  lgsquadlem2  27312  m1lgs  27319  cuteq0  27769  precsexlem11  28148  seqsval  28211  n0sbday  28273  zseo  28338  mirauto  28655  lmiisolem  28767  ttglem  28847  axlowdimlem16  28928  ebtwntg  28953  ecgrtg  28954  elntg2  28956  nbgrval  29307  uvtxupgrres  29379  clwlknf1oclwwlknlem3  30053  eucrct2eupth  30215  smcnlem  30667  siii  30823  pjhthlem1  31361  sbcies  32457  imadifxp  32571  dfimafnf  32608  funcnvmpt  32639  ccatws1f1olast  32923  gsumwun  33035  symgcom  33042  cycpmconjslem1  33113  rloc0g  33228  rloc1r  33229  resvlem  33288  qusker  33304  elrspunsn  33384  opprqusplusg  33444  idlsrgbas  33459  idlsrgplusg  33460  idlsrgmulr  33462  idlsrgtset  33463  idlsrgmulrval  33464  fldextrspundgdvdslem  33683  fldextrspundgdvds  33684  irredminply  33719  algextdeglem4  33723  algextdeglem5  33724  constrrtcc  33738  cos9thpinconstrlem1  33792  mdetpmtr12  33828  zarcls  33877  zar0ring  33881  pstmval  33898  xpinpreima2  33910  pnfneige0  33954  zlmds  33965  zlmtset  33966  esumid  34047  esumrnmpt  34055  sxsigon  34195  carsgclctunlem1  34320  circlemethnat  34644  fnrelpredd  35091  f1resfz0f1d  35126  pthhashvtx  35140  filnetlem4  36394  setsstrset  37149  finxpreclem4  37407  itg2addnclem  37690  iblabsnclem  37702  areacirc  37732  fnopabco  37742  heiborlem8  37837  rngoi  37918  drngoi  37970  ldualvsub  39173  dalemrotyz  39676  dalem6  39686  dalem7  39687  dalem11  39692  dalem12  39693  dalemrotps  39709  dalem30  39720  dalem35  39725  cdleme1  40245  cdleme9  40271  cdleme20c  40329  cdleme20d  40330  cdlemefrs29clN  40417  cdleme37m  40480  cdleme43aN  40507  cdlemg1b2  40589  cdlemg4f  40633  cdlemh2  40834  erngdvlem1  41006  erngdvlem2N  41007  erngdvlem3  41008  erngdvlem4  41009  erngdvlem1-rN  41014  erngdvlem2-rN  41015  erngdvlem3-rN  41016  erngdvlem4-rN  41017  dvh4dimN  41465  lcdvsub  41635  hlhilsca  41953  hlhilbase  41954  hlhilplus  41955  hlhilvsca  41965  hlhilip  41966  hlhilipval  41967  reelznn0nn  42473  rnasclg  42511  evlsval3  42571  prjspeclsp  42624  mzpcompact2lem  42763  eldioph2lem1  42772  fiphp3d  42831  rmxypairf1o  42923  wopprc  43042  lmhmlnmsplit  43099  rp-tfslim  43365  onsucunitp  43385  clcnvlem  43635  mnringnmulrd  44226  mnringbaserd  44228  mnringmulrd  44235  dmmptdff  45239  dmmptdf2  45249  ellimcabssub0  45636  cosknegpi  45886  dvnprodlem1  45963  fourierdlem58  46181  fourierdlem59  46182  fourierdlem72  46195  fourierdlem80  46203  sqwvfourb  46246  etransclem28  46279  etransclem41  46292  omef  46513  dfaimafn  47175  afv2co2  47267  sbgoldbo  47797  rrxlinesc  48746  rrxlinec  48747  rrx2linest2  48755  rrxsphere  48759  itsclinecirc0b  48785  itsclquadb  48787  2oppf  49143  idfullsubc  49172  oppc1stf  49299  oppc2ndf  49300  dfinito4  49512  prstcnid  49564  prstcthin  49572