Theorem eqtr4id 2817

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  rabeqcda  3427  iftrue  4491  iffalse  4494  difprsn1  4763  csbcnv  5871  dmmptg  6256  setlikespec  6346  funimacnv  6643  dmmptd  6706  resasplit  6774  dffv3  6904  dfimafn  6970  fniinfv  6986  dffv2  7003  fvco2  7005  funcnvmpt  7018  fniunfv  7274  isoini  7369  fvmpopr2d  7606  zfrep6OLD  7991  oprabco  8133  suppco  8251  oeeulem  8638  ixpconstg  8962  sbthlem4  9137  sbthlem5  9138  sbthlem6  9139  supval2  9474  hartogslem1  9563  cantnflem1d  9716  alephsuc2  10186  dfac3  10227  hsmexlem5  10535  axdc2lem  10553  gruima  10914  eqneg  12064  zeo  12812  fseq1p1m1  13759  f1resfz0f1d  13954  hashfzo  14601  hashimarn  14612  wrdval  14688  wrdnval  14717  repswswrd  14963  s1co  15012  swrds2  15120  s7f1o  15148  modfsummod  15990  telfsumo  15998  indsumhash  16025  mulgcd  16750  algcvg  16780  phiprmpw  16982  phisum  16997  strfv3  17411  resseqnbas  17449  pwssnf1o  17699  imassca  17720  homfeq  17897  oppcbas  17921  resscatc  18313  estrcbasbas  18334  funcestrcsetclem7  18349  funcestrcsetclem8  18350  funcestrcsetclem9  18351  fthestrcsetc  18353  fullestrcsetc  18354  equivestrcsetc  18355  setc1strwun  18356  funcsetcestrclem7  18364  funcsetcestrclem8  18365  funcsetcestrclem9  18366  fthsetcestrc  18368  fullsetcestrc  18369  lubsn  18685  ipotset  18736  ipole  18737  plusfeq  18853  idressidex0  18889  pws0g  18996  frmd0  19085  efmndtset  19104  oppgplusfval  19592  gsmsymgrfix  19672  gsmsymgreq  19676  psgnunilem2  19739  sylow3lem2  19872  oppglsm  19886  frgpuplem  20016  frgpupf  20017  frgpup1  20019  frgpup3lem  20021  gsumzoppg  20188  ablfac1eu  20319  pgpfaclem1  20327  pwsmgp  20586  opprmulfval  20599  rdivmuldivd  20673  dfrhm2  20734  subrg1  20864  staffn  21130  issrngd  21142  scafeq  21187  lbsextlem4  21469  sralem  21481  sravsca  21486  sraip  21487  2idlbas  21587  zlmlem  21852  zlmvsca  21857  znbaslem  21874  ipfeq  21986  ssipeq  21992  thlbas  22032  thlle  22033  thloc  22035  dsmmbase  22071  dsmmelbas  22075  frlmelbas  22092  frlmphl  22117  islindf4  22174  rnascl  22229  psrlinv  22293  opsrbaslem  22388  evlseu  22422  evlsval3  22428  mpfsubrg  22450  psdmvr  22520  evl1sca  22682  evls1var  22686  matbas  22758  matplusg  22759  matsca  22760  matvsca  22761  matbas2d  22768  matsubgcell  22779  matmulcell  22790  ofco2  22796  mattposm  22804  mat1f1o  22823  mdetunilem8  22964  madugsum  22988  cramerimplem2  23032  decpmatmullem  23119  paste  23642  ptpjcn  23960  uptx  23974  xpstopnlem1  24158  alexsubALTlem4  24399  cnextf  24415  submtmd  24453  ussval  24608  tuslem  24615  psmetge0  24661  xmetge0  24693  setsmsds  24825  sgrim  24980  tnglem  24989  tngtset  24998  tngngp2  25001  resubmet  25151  pcorev2  25379  om1plusg  25385  om1tset  25386  om1opn  25387  pi1grplem  25400  clmadd  25425  clmmul  25426  clmcj  25427  tcphtopn  25577  tchnmfval  25579  bcthlem1  25675  bcthlem2  25676  bcthlem4  25678  bcth3  25682  rrxmval  25756  rrxmfval  25757  rrxdsfi  25762  ehlbase  25766  minveclem3b  25779  pjthlem1  25788  volun  25896  voliun  25905  uniioovol  25930  itg2i1fseq  26106  itgcnlem  26140  iblabslem  26178  limcres  26236  cnplimc  26237  ply1termlem  26551  0dgr  26594  taylthlem1  26730  abelth  26798  lawcos  27174  lgambdd  27394  basellem8  27445  musum  27548  chtub  27569  dchrval  27591  dchrinvcl  27610  lgsval4lem  27665  lgsquadlem2  27738  m1lgs  27745  cuteq0  28231  precsexlem11  28633  seqsval  28704  n0bday  28768  zseo  28838  mirauto  29186  lmiisolem  29331  ttglem  29483  axlowdimlem16  29565  ebtwntg  29590  ecgrtg  29591  elntg2  29593  nbgrval  29947  uvtxupgrres  30019  pthhashvtx  30345  clwlknf1oclwwlknlem3  30704  eucrct2eupth  30876  smcnlem  31329  siii  31485  pjhthlem1  32023  sbcies  33156  imadifxp  33267  dfimafnf  33302  ccatws1f1olast  33585  gsummulsubdishift1  33699  gsumwun  33707  symgcom  33714  cycpmconjslem1  33785  rloc0g  33903  rloc1r  33904  resvlem  33964  qusker  33980  elrspunsn  34049  opprqusplusg  34083  idlsrgbas  34106  idlsrgplusg  34107  idlsrgmulr  34109  idlsrgtset  34110  idlsrgmulrval  34111  fldextrspundgdvdslem  34382  fldextrspundgdvds  34383  irredminply  34418  algextdeglem4  34422  algextdeglem5  34423  constrrtcc  34437  cos9thpinconstrlem1  34491  mdetpmtr12  34527  zarcls  34576  zar0ring  34580  pstmval  34597  xpinpreima2  34609  pnfneige0  34653  zlmds  34664  zlmtset  34665  esumid  34746  esumrnmpt  34754  sxsigon  34895  carsgclctunlem1  35019  circlemethnat  35340  fnrelpredd  35804  filnetlem4  37347  setsstrset  38247  finxpreclem4  38509  itg2addnclem  38781  iblabsnclem  38793  areacirc  38823  fnopabco  38849  heiborlem8  38944  rngoi  39025  drngoi  39077  ldualvsub  40404  dalemrotyz  40907  dalem6  40917  dalem7  40918  dalem11  40923  dalem12  40924  dalemrotps  40940  dalem30  40951  dalem35  40956  cdleme1  41476  cdleme9  41502  cdleme20c  41560  cdleme20d  41561  cdlemefrs29clN  41648  cdleme37m  41711  cdleme43aN  41738  cdlemg1b2  41820  cdlemg4f  41864  cdlemh2  42065  erngdvlem1  42237  erngdvlem2N  42238  erngdvlem3  42239  erngdvlem4  42240  erngdvlem1-rN  42245  erngdvlem2-rN  42246  erngdvlem3-rN  42247  erngdvlem4-rN  42248  dvh4dimN  42696  lcdvsub  42866  hlhilsca  43184  hlhilbase  43185  hlhilplus  43186  hlhilvsca  43196  hlhilip  43197  hlhilipval  43198  25or6to4  43448  reelznn0nn  43718  rnasclg  43756  prjspeclsp  43833  mzpcompact2lem  43955  eldioph2lem1  43964  fiphp3d  44019  rmxypairf1o  44111  wopprc  44230  lmhmlnmsplit  44282  rp-tfslim  44547  onsucunitp  44567  clcnvlem  44815  mnringnmulrd  45404  mnringbaserd  45406  mnringmulrd  45413  dmmptdff  46441  dmmptdf2  46450  ellimcabssub0  46834  cosknegpi  47084  dvnprodlem1  47161  fourierdlem58  47379  fourierdlem59  47380  fourierdlem72  47393  fourierdlem80  47401  sqwvfourb  47444  etransclem28  47477  etransclem41  47490  omef  47711  dfaimafn  48440  afv2co2  48532  sbgoldbo  49090  rrxlinesc  50053  rrxlinec  50054  rrx2linest2  50061  rrxsphere  50065  itsclinecirc0b  50091  itsclquadb  50093  2oppf  50453  idfullsubc  50482  oppc1stf  50615  oppc2ndf  50616  dfinito4  50841  prstcnid  50896  prstcthin  50904