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 2745	. 2 ⊢ 𝐵 = 𝐴
4	1, 3	eqtr2di 2788	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 2123  ax-ext 2708

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

This theorem is referenced by:  rabeqcda  3410  iftrue  4485  iffalse  4488  difprsn1  4756  dmmptg  6200  setlikespec  6283  funimacnv  6573  dmmptd  6637  resasplit  6704  dffv3  6830  dfimafn  6896  fniinfv  6912  dffv2  6929  fvco2  6931  fniunfv  7193  isoini  7284  fvmpopr2d  7520  zfrep6  7899  oprabco  8038  suppco  8148  oeeulem  8529  ixpconstg  8844  sbthlem4  9018  sbthlem5  9019  sbthlem6  9020  supval2  9358  hartogslem1  9447  cantnflem1d  9597  alephsuc2  9990  dfac3  10031  hsmexlem5  10340  axdc2lem  10358  gruima  10713  eqneg  11861  zeo  12578  fseq1p1m1  13514  hashfzo  14352  hashimarn  14363  wrdval  14439  wrdnval  14468  repswswrd  14707  s1co  14756  swrds2  14863  s7f1o  14889  modfsummod  15717  telfsumo  15725  mulgcd  16475  algcvg  16503  phiprmpw  16703  phisum  16718  strfv3  17131  resseqnbas  17169  pwssnf1o  17419  imassca  17440  homfeq  17617  oppcbas  17641  resscatc  18033  estrcbasbas  18054  funcestrcsetclem7  18069  funcestrcsetclem8  18070  funcestrcsetclem9  18071  fthestrcsetc  18073  fullestrcsetc  18074  equivestrcsetc  18075  setc1strwun  18076  funcsetcestrclem7  18084  funcsetcestrclem8  18085  funcsetcestrclem9  18086  fthsetcestrc  18088  fullsetcestrc  18089  lubsn  18405  ipotset  18456  ipole  18457  plusfeq  18573  pws0g  18698  frmd0  18785  efmndtset  18804  oppgplusfval  19277  gsmsymgrfix  19357  gsmsymgreq  19361  psgnunilem2  19424  sylow3lem2  19557  oppglsm  19571  frgpuplem  19701  frgpupf  19702  frgpup1  19704  frgpup3lem  19706  gsumzoppg  19873  ablfac1eu  20004  pgpfaclem1  20012  pwsmgp  20262  opprmulfval  20275  rdivmuldivd  20349  dfrhm2  20410  subrg1  20515  staffn  20776  issrngd  20788  scafeq  20833  lbsextlem4  21116  sralem  21128  sravsca  21133  sraip  21134  2idlbas  21218  zlmlem  21471  zlmvsca  21476  znbaslem  21493  ipfeq  21605  ssipeq  21611  thlbas  21651  thlle  21652  thloc  21654  dsmmbase  21690  dsmmelbas  21694  frlmelbas  21711  frlmphl  21736  islindf4  21793  rnascl  21847  psrlinv  21911  opsrbaslem  22004  evlseu  22038  evlsval3  22044  mpfsubrg  22066  psdmvr  22112  ply1scl0OLD  22233  evl1sca  22278  evls1var  22282  matbas  22357  matplusg  22358  matsca  22359  matvsca  22360  matbas2d  22367  matsubgcell  22378  matmulcell  22389  ofco2  22395  mattposm  22403  mat1f1o  22422  mdetunilem8  22563  madugsum  22587  cramerimplem2  22628  decpmatmullem  22715  paste  23238  ptpjcn  23555  uptx  23569  xpstopnlem1  23753  alexsubALTlem4  23994  cnextf  24010  submtmd  24048  ussval  24203  tuslem  24210  psmetge0  24256  xmetge0  24288  setsmsds  24420  sgrim  24575  tnglem  24584  tngtset  24593  tngngp2  24596  resubmet  24746  pcorev2  24984  om1plusg  24990  om1tset  24991  om1opn  24992  pi1grplem  25005  clmadd  25030  clmmul  25031  clmcj  25032  tcphtopn  25182  tchnmfval  25184  bcthlem1  25280  bcthlem2  25281  bcthlem4  25283  bcth3  25287  rrxmval  25361  rrxmfval  25362  rrxdsfi  25367  ehlbase  25371  minveclem3b  25384  pjthlem1  25393  volun  25502  voliun  25511  uniioovol  25536  itg2i1fseq  25712  itgcnlem  25747  iblabslem  25785  limcres  25843  cnplimc  25844  ply1termlem  26164  0dgr  26206  taylthlem1  26337  abelth  26407  lawcos  26782  lgambdd  27003  basellem8  27054  musum  27157  chtub  27179  dchrval  27201  dchrinvcl  27220  lgsval4lem  27275  lgsquadlem2  27348  m1lgs  27355  cuteq0  27811  precsexlem11  28213  seqsval  28284  n0bday  28348  zseo  28418  mirauto  28756  lmiisolem  28868  ttglem  28948  axlowdimlem16  29030  ebtwntg  29055  ecgrtg  29056  elntg2  29058  nbgrval  29409  uvtxupgrres  29481  clwlknf1oclwwlknlem3  30158  eucrct2eupth  30320  smcnlem  30772  siii  30928  pjhthlem1  31466  sbcies  32562  imadifxp  32676  dfimafnf  32714  funcnvmpt  32745  ccatws1f1olast  33034  gsummulsubdishift1  33151  gsumwun  33158  symgcom  33165  cycpmconjslem1  33236  rloc0g  33353  rloc1r  33354  resvlem  33414  qusker  33430  elrspunsn  33510  opprqusplusg  33570  idlsrgbas  33585  idlsrgplusg  33586  idlsrgmulr  33588  idlsrgtset  33589  idlsrgmulrval  33590  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  irredminply  33873  algextdeglem4  33877  algextdeglem5  33878  constrrtcc  33892  cos9thpinconstrlem1  33946  mdetpmtr12  33982  zarcls  34031  zar0ring  34035  pstmval  34052  xpinpreima2  34064  pnfneige0  34108  zlmds  34119  zlmtset  34120  esumid  34201  esumrnmpt  34209  sxsigon  34349  carsgclctunlem1  34474  circlemethnat  34798  fnrelpredd  35247  f1resfz0f1d  35308  pthhashvtx  35322  filnetlem4  36575  setsstrset  37341  finxpreclem4  37599  itg2addnclem  37872  iblabsnclem  37884  areacirc  37914  fnopabco  37924  heiborlem8  38019  rngoi  38100  drngoi  38152  ldualvsub  39415  dalemrotyz  39918  dalem6  39928  dalem7  39929  dalem11  39934  dalem12  39935  dalemrotps  39951  dalem30  39962  dalem35  39967  cdleme1  40487  cdleme9  40513  cdleme20c  40571  cdleme20d  40572  cdlemefrs29clN  40659  cdleme37m  40722  cdleme43aN  40749  cdlemg1b2  40831  cdlemg4f  40875  cdlemh2  41076  erngdvlem1  41248  erngdvlem2N  41249  erngdvlem3  41250  erngdvlem4  41251  erngdvlem1-rN  41256  erngdvlem2-rN  41257  erngdvlem3-rN  41258  erngdvlem4-rN  41259  dvh4dimN  41707  lcdvsub  41877  hlhilsca  42195  hlhilbase  42196  hlhilplus  42197  hlhilvsca  42207  hlhilip  42208  hlhilipval  42209  reelznn0nn  42716  rnasclg  42754  prjspeclsp  42855  mzpcompact2lem  42993  eldioph2lem1  43002  fiphp3d  43061  rmxypairf1o  43153  wopprc  43272  lmhmlnmsplit  43329  rp-tfslim  43595  onsucunitp  43615  clcnvlem  43864  mnringnmulrd  44455  mnringbaserd  44457  mnringmulrd  44464  dmmptdff  45467  dmmptdf2  45477  ellimcabssub0  45863  cosknegpi  46113  dvnprodlem1  46190  fourierdlem58  46408  fourierdlem59  46409  fourierdlem72  46422  fourierdlem80  46430  sqwvfourb  46473  etransclem28  46506  etransclem41  46519  omef  46740  dfaimafn  47411  afv2co2  47503  sbgoldbo  48033  rrxlinesc  48981  rrxlinec  48982  rrx2linest2  48990  rrxsphere  48994  itsclinecirc0b  49020  itsclquadb  49022  2oppf  49377  idfullsubc  49406  oppc1stf  49533  oppc2ndf  49534  dfinito4  49746  prstcnid  49798  prstcthin  49806