Theorem eqtr4id 2790

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 2740	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2788	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  rabeqcda  3442  iftrue  4534  iffalse  4537  difprsn1  4803  dmmptg  6241  setlikespec  6326  funimacnv  6629  dmmptd  6695  resasplit  6761  dffv3  6887  dfimafn  6954  fniinfv  6969  dffv2  6986  fvco2  6988  fniunfv  7249  isoini  7338  fvmpopr2d  7572  zfrep6  7944  oprabco  8085  suppco  8194  oeeulem  8604  ixpconstg  8903  sbthlem4  9089  sbthlem5  9090  sbthlem6  9091  supval2  9453  hartogslem1  9540  cantnflem1d  9686  alephsuc2  10078  dfac3  10119  hsmexlem5  10428  axdc2lem  10446  gruima  10800  eqneg  11939  zeo  12653  fseq1p1m1  13580  hashfzo  14394  hashimarn  14405  wrdval  14472  wrdnval  14500  repswswrd  14739  s1co  14789  swrds2  14896  modfsummod  15745  telfsumo  15753  mulgcd  16495  algcvg  16518  phiprmpw  16714  phisum  16728  strfv3  17143  resseqnbas  17191  resslemOLD  17192  pwssnf1o  17449  imassca  17470  homfeq  17643  oppcbas  17668  oppcbasOLD  17669  resscatc  18064  estrcbasbas  18087  funcestrcsetclem7  18103  funcestrcsetclem8  18104  funcestrcsetclem9  18105  fthestrcsetc  18107  fullestrcsetc  18108  equivestrcsetc  18109  setc1strwun  18110  funcsetcestrclem7  18118  funcsetcestrclem8  18119  funcsetcestrclem9  18120  fthsetcestrc  18122  fullsetcestrc  18123  lubsn  18440  ipotset  18491  ipole  18492  plusfeq  18574  pws0g  18696  frmd0  18778  efmndtset  18797  oppgplusfval  19254  gsmsymgrfix  19338  gsmsymgreq  19342  psgnunilem2  19405  sylow3lem2  19538  oppglsm  19552  frgpuplem  19682  frgpupf  19683  frgpup1  19685  frgpup3lem  19687  gsumzoppg  19854  ablfac1eu  19985  pgpfaclem1  19993  pwsmgp  20216  opprmulfval  20228  rdivmuldivd  20305  dfrhm2  20366  subrg1  20473  staffn  20601  issrngd  20613  scafeq  20637  lbsextlem4  20920  sralem  20936  sralemOLD  20937  sravsca  20946  sravscaOLD  20947  sraip  20948  2idlbas  21019  zlmlem  21286  zlmlemOLD  21287  zlmvsca  21295  znbaslem  21310  znbaslemOLD  21311  ipfeq  21423  ssipeq  21429  thlbas  21469  thlbasOLD  21470  thlle  21471  thlleOLD  21472  thloc  21474  dsmmbase  21510  dsmmelbas  21514  frlmelbas  21531  frlmphl  21556  islindf4  21613  rnascl  21665  psrlinv  21736  opsrbaslem  21824  opsrbaslemOLD  21825  evlseu  21866  mpfsubrg  21886  ply1scl0OLD  22034  evl1sca  22074  evls1var  22078  matbas  22134  matplusg  22135  matsca  22136  matscaOLD  22137  matvsca  22138  matvscaOLD  22139  matbas2d  22146  matsubgcell  22157  matmulcell  22168  ofco2  22174  mattposm  22182  mat1f1o  22201  mdetunilem8  22342  madugsum  22366  cramerimplem2  22407  decpmatmullem  22494  paste  23019  ptpjcn  23336  uptx  23350  xpstopnlem1  23534  alexsubALTlem4  23775  cnextf  23791  submtmd  23829  ussval  23985  tuslem  23992  tuslemOLD  23993  psmetge0  24039  xmetge0  24071  setsmsds  24204  setsmsdsOLD  24205  sgrim  24361  tnglem  24370  tnglemOLD  24371  tngtset  24387  tngngp2  24390  resubmet  24539  pcorev2  24776  om1plusg  24782  om1tset  24783  om1opn  24784  pi1grplem  24797  clmadd  24822  clmmul  24823  clmcj  24824  tcphtopn  24975  tchnmfval  24977  bcthlem1  25073  bcthlem2  25074  bcthlem4  25076  bcth3  25080  rrxmval  25154  rrxmfval  25155  rrxdsfi  25160  ehlbase  25164  minveclem3b  25177  pjthlem1  25186  volun  25295  voliun  25304  uniioovol  25329  itg2i1fseq  25506  itgcnlem  25540  iblabslem  25578  limcres  25636  cnplimc  25637  ply1termlem  25953  0dgr  25995  taylthlem1  26122  abelth  26190  lawcos  26558  lgambdd  26778  basellem8  26829  musum  26932  chtub  26952  dchrval  26974  dchrinvcl  26993  lgsval4lem  27048  lgsquadlem2  27121  m1lgs  27128  cuteq0  27571  precsexlem11  27903  mirauto  28203  lmiisolem  28315  ttglem  28396  ttglemOLD  28397  axlowdimlem16  28483  ebtwntg  28508  ecgrtg  28509  elntg2  28511  nbgrval  28861  uvtxupgrres  28933  clwlknf1oclwwlknlem3  29604  eucrct2eupth  29766  smcnlem  30218  siii  30374  pjhthlem1  30912  sbcies  31996  imadifxp  32100  dfimafnf  32128  funcnvmpt  32160  symgcom  32515  cycpmconjslem1  32584  resvlem  32716  resvlemOLD  32717  qusker  32735  elrspunsn  32822  opprqusplusg  32878  idlsrgbas  32893  idlsrgplusg  32894  idlsrgmulr  32896  idlsrgtset  32897  idlsrgmulrval  32898  algextdeglem4  33066  algextdeglem5  33067  mdetpmtr12  33104  zarcls  33153  zar0ring  33157  pstmval  33174  xpinpreima2  33186  pnfneige0  33230  zlmds  33241  zlmdsOLD  33242  zlmtset  33243  zlmtsetOLD  33244  esumid  33341  esumrnmpt  33349  sxsigon  33489  carsgclctunlem1  33615  circlemethnat  33952  fnrelpredd  34391  f1resfz0f1d  34402  pthhashvtx  34417  filnetlem4  35570  setsstrset  36321  finxpreclem4  36579  itg2addnclem  36843  iblabsnclem  36855  areacirc  36885  fnopabco  36895  heiborlem8  36990  rngoi  37071  drngoi  37123  ldualvsub  38329  dalemrotyz  38833  dalem6  38843  dalem7  38844  dalem11  38849  dalem12  38850  dalemrotps  38866  dalem30  38877  dalem35  38882  cdleme1  39402  cdleme9  39428  cdleme20c  39486  cdleme20d  39487  cdlemefrs29clN  39574  cdleme37m  39637  cdleme43aN  39664  cdlemg1b2  39746  cdlemg4f  39790  cdlemh2  39991  erngdvlem1  40163  erngdvlem2N  40164  erngdvlem3  40165  erngdvlem4  40166  erngdvlem1-rN  40171  erngdvlem2-rN  40172  erngdvlem3-rN  40173  erngdvlem4-rN  40174  dvh4dimN  40622  lcdvsub  40792  hlhilsca  41110  hlhilbase  41111  hlhilplus  41112  hlhilvsca  41126  hlhilip  41127  hlhilipval  41128  rnasclg  41380  evlsval3  41434  reelznn0nn  41625  prjspeclsp  41657  mzpcompact2lem  41792  eldioph2lem1  41801  fiphp3d  41860  rmxypairf1o  41953  wopprc  42072  lmhmlnmsplit  42132  rp-tfslim  42406  onsucunitp  42426  clcnvlem  42677  mnringnmulrd  43271  mnringnmulrdOLD  43272  mnringbaserd  43275  mnringmulrd  43283  dmmptdff  44221  dmmptdf2  44234  ellimcabssub0  44632  cosknegpi  44884  fourierdlem58  45179  fourierdlem59  45180  fourierdlem72  45193  fourierdlem80  45201  sqwvfourb  45244  etransclem28  45277  etransclem41  45290  omef  45511  dfaimafn  46172  afv2co2  46264  sbgoldbo  46754  rrxlinesc  47509  rrxlinec  47510  rrx2linest2  47518  rrxsphere  47522  itsclinecirc0b  47548  itsclquadb  47550  prstcnid  47774  prstcthin  47784