Theorem eqtr4id 2791

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  rabeqcda  3411  iftrue  4486  iffalse  4489  difprsn1  4757  dmmptg  6201  setlikespec  6284  funimacnv  6574  dmmptd  6638  resasplit  6705  dffv3  6831  dfimafn  6897  fniinfv  6913  dffv2  6930  fvco2  6932  funcnvmpt  6944  fniunfv  7195  isoini  7286  fvmpopr2d  7522  zfrep6  7901  oprabco  8040  suppco  8150  oeeulem  8531  ixpconstg  8848  sbthlem4  9022  sbthlem5  9023  sbthlem6  9024  supval2  9362  hartogslem1  9451  cantnflem1d  9601  alephsuc2  9994  dfac3  10035  hsmexlem5  10344  axdc2lem  10362  gruima  10717  eqneg  11865  zeo  12582  fseq1p1m1  13518  hashfzo  14356  hashimarn  14367  wrdval  14443  wrdnval  14472  repswswrd  14711  s1co  14760  swrds2  14867  s7f1o  14893  modfsummod  15721  telfsumo  15729  mulgcd  16479  algcvg  16507  phiprmpw  16707  phisum  16722  strfv3  17135  resseqnbas  17173  pwssnf1o  17423  imassca  17444  homfeq  17621  oppcbas  17645  resscatc  18037  estrcbasbas  18058  funcestrcsetclem7  18073  funcestrcsetclem8  18074  funcestrcsetclem9  18075  fthestrcsetc  18077  fullestrcsetc  18078  equivestrcsetc  18079  setc1strwun  18080  funcsetcestrclem7  18088  funcsetcestrclem8  18089  funcsetcestrclem9  18090  fthsetcestrc  18092  fullsetcestrc  18093  lubsn  18409  ipotset  18460  ipole  18461  plusfeq  18577  pws0g  18702  frmd0  18789  efmndtset  18808  oppgplusfval  19281  gsmsymgrfix  19361  gsmsymgreq  19365  psgnunilem2  19428  sylow3lem2  19561  oppglsm  19575  frgpuplem  19705  frgpupf  19706  frgpup1  19708  frgpup3lem  19710  gsumzoppg  19877  ablfac1eu  20008  pgpfaclem1  20016  pwsmgp  20266  opprmulfval  20279  rdivmuldivd  20353  dfrhm2  20414  subrg1  20519  staffn  20780  issrngd  20792  scafeq  20837  lbsextlem4  21120  sralem  21132  sravsca  21137  sraip  21138  2idlbas  21222  zlmlem  21475  zlmvsca  21480  znbaslem  21497  ipfeq  21609  ssipeq  21615  thlbas  21655  thlle  21656  thloc  21658  dsmmbase  21694  dsmmelbas  21698  frlmelbas  21715  frlmphl  21740  islindf4  21797  rnascl  21851  psrlinv  21915  opsrbaslem  22008  evlseu  22042  evlsval3  22048  mpfsubrg  22070  psdmvr  22116  ply1scl0OLD  22237  evl1sca  22282  evls1var  22286  matbas  22361  matplusg  22362  matsca  22363  matvsca  22364  matbas2d  22371  matsubgcell  22382  matmulcell  22393  ofco2  22399  mattposm  22407  mat1f1o  22426  mdetunilem8  22567  madugsum  22591  cramerimplem2  22632  decpmatmullem  22719  paste  23242  ptpjcn  23559  uptx  23573  xpstopnlem1  23757  alexsubALTlem4  23998  cnextf  24014  submtmd  24052  ussval  24207  tuslem  24214  psmetge0  24260  xmetge0  24292  setsmsds  24424  sgrim  24579  tnglem  24588  tngtset  24597  tngngp2  24600  resubmet  24750  pcorev2  24988  om1plusg  24994  om1tset  24995  om1opn  24996  pi1grplem  25009  clmadd  25034  clmmul  25035  clmcj  25036  tcphtopn  25186  tchnmfval  25188  bcthlem1  25284  bcthlem2  25285  bcthlem4  25287  bcth3  25291  rrxmval  25365  rrxmfval  25366  rrxdsfi  25371  ehlbase  25375  minveclem3b  25388  pjthlem1  25397  volun  25506  voliun  25515  uniioovol  25540  itg2i1fseq  25716  itgcnlem  25751  iblabslem  25789  limcres  25847  cnplimc  25848  ply1termlem  26168  0dgr  26210  taylthlem1  26341  abelth  26411  lawcos  26786  lgambdd  27007  basellem8  27058  musum  27161  chtub  27183  dchrval  27205  dchrinvcl  27224  lgsval4lem  27279  lgsquadlem2  27352  m1lgs  27359  cuteq0  27813  precsexlem11  28198  seqsval  28269  n0sbday  28332  zseo  28401  mirauto  28739  lmiisolem  28851  ttglem  28931  axlowdimlem16  29013  ebtwntg  29038  ecgrtg  29039  elntg2  29041  nbgrval  29392  uvtxupgrres  29464  clwlknf1oclwwlknlem3  30141  eucrct2eupth  30303  smcnlem  30755  siii  30911  pjhthlem1  31449  sbcies  32544  imadifxp  32658  dfimafnf  32696  ccatws1f1olast  33015  gsummulsubdishift1  33132  gsumwun  33139  symgcom  33146  cycpmconjslem1  33217  rloc0g  33334  rloc1r  33335  resvlem  33395  qusker  33411  elrspunsn  33491  opprqusplusg  33551  idlsrgbas  33566  idlsrgplusg  33567  idlsrgmulr  33569  idlsrgtset  33570  idlsrgmulrval  33571  fldextrspundgdvdslem  33818  fldextrspundgdvds  33819  irredminply  33854  algextdeglem4  33858  algextdeglem5  33859  constrrtcc  33873  cos9thpinconstrlem1  33927  mdetpmtr12  33963  zarcls  34012  zar0ring  34016  pstmval  34033  xpinpreima2  34045  pnfneige0  34089  zlmds  34100  zlmtset  34101  esumid  34182  esumrnmpt  34190  sxsigon  34330  carsgclctunlem1  34455  circlemethnat  34779  fnrelpredd  35228  f1resfz0f1d  35289  pthhashvtx  35303  filnetlem4  36556  setsstrset  37312  finxpreclem4  37570  itg2addnclem  37843  iblabsnclem  37855  areacirc  37885  fnopabco  37895  heiborlem8  37990  rngoi  38071  drngoi  38123  ldualvsub  39452  dalemrotyz  39955  dalem6  39965  dalem7  39966  dalem11  39971  dalem12  39972  dalemrotps  39988  dalem30  39999  dalem35  40004  cdleme1  40524  cdleme9  40550  cdleme20c  40608  cdleme20d  40609  cdlemefrs29clN  40696  cdleme37m  40759  cdleme43aN  40786  cdlemg1b2  40868  cdlemg4f  40912  cdlemh2  41113  erngdvlem1  41285  erngdvlem2N  41286  erngdvlem3  41287  erngdvlem4  41288  erngdvlem1-rN  41293  erngdvlem2-rN  41294  erngdvlem3-rN  41295  erngdvlem4-rN  41296  dvh4dimN  41744  lcdvsub  41914  hlhilsca  42232  hlhilbase  42233  hlhilplus  42234  hlhilvsca  42244  hlhilip  42245  hlhilipval  42246  reelznn0nn  42752  rnasclg  42790  prjspeclsp  42891  mzpcompact2lem  43029  eldioph2lem1  43038  fiphp3d  43097  rmxypairf1o  43189  wopprc  43308  lmhmlnmsplit  43365  rp-tfslim  43631  onsucunitp  43651  clcnvlem  43900  mnringnmulrd  44491  mnringbaserd  44493  mnringmulrd  44500  dmmptdff  45503  dmmptdf2  45513  ellimcabssub0  45899  cosknegpi  46149  dvnprodlem1  46226  fourierdlem58  46444  fourierdlem59  46445  fourierdlem72  46458  fourierdlem80  46466  sqwvfourb  46509  etransclem28  46542  etransclem41  46555  omef  46776  dfaimafn  47447  afv2co2  47539  sbgoldbo  48069  rrxlinesc  49017  rrxlinec  49018  rrx2linest2  49026  rrxsphere  49030  itsclinecirc0b  49056  itsclquadb  49058  2oppf  49413  idfullsubc  49442  oppc1stf  49569  oppc2ndf  49570  dfinito4  49782  prstcnid  49834  prstcthin  49842