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 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  rabeqcda  3420  iftrue  4497  iffalse  4500  difprsn1  4767  dmmptg  6218  setlikespec  6301  funimacnv  6600  dmmptd  6666  resasplit  6733  dffv3  6857  dfimafn  6926  fniinfv  6942  dffv2  6959  fvco2  6961  fniunfv  7224  isoini  7316  fvmpopr2d  7554  zfrep6  7936  oprabco  8078  suppco  8188  oeeulem  8568  ixpconstg  8882  sbthlem4  9060  sbthlem5  9061  sbthlem6  9062  supval2  9413  hartogslem1  9502  cantnflem1d  9648  alephsuc2  10040  dfac3  10081  hsmexlem5  10390  axdc2lem  10408  gruima  10762  eqneg  11909  zeo  12627  fseq1p1m1  13566  hashfzo  14401  hashimarn  14412  wrdval  14488  wrdnval  14517  repswswrd  14756  s1co  14806  swrds2  14913  s7f1o  14939  modfsummod  15767  telfsumo  15775  mulgcd  16525  algcvg  16553  phiprmpw  16753  phisum  16768  strfv3  17181  resseqnbas  17219  pwssnf1o  17468  imassca  17489  homfeq  17662  oppcbas  17686  resscatc  18078  estrcbasbas  18099  funcestrcsetclem7  18114  funcestrcsetclem8  18115  funcestrcsetclem9  18116  fthestrcsetc  18118  fullestrcsetc  18119  equivestrcsetc  18120  setc1strwun  18121  funcsetcestrclem7  18129  funcsetcestrclem8  18130  funcsetcestrclem9  18131  fthsetcestrc  18133  fullsetcestrc  18134  lubsn  18448  ipotset  18499  ipole  18500  plusfeq  18582  pws0g  18707  frmd0  18794  efmndtset  18813  oppgplusfval  19287  gsmsymgrfix  19365  gsmsymgreq  19369  psgnunilem2  19432  sylow3lem2  19565  oppglsm  19579  frgpuplem  19709  frgpupf  19710  frgpup1  19712  frgpup3lem  19714  gsumzoppg  19881  ablfac1eu  20012  pgpfaclem1  20020  pwsmgp  20243  opprmulfval  20255  rdivmuldivd  20329  dfrhm2  20390  subrg1  20498  staffn  20759  issrngd  20771  scafeq  20795  lbsextlem4  21078  sralem  21090  sravsca  21095  sraip  21096  2idlbas  21180  zlmlem  21433  zlmvsca  21438  znbaslem  21455  ipfeq  21566  ssipeq  21572  thlbas  21612  thlle  21613  thloc  21615  dsmmbase  21651  dsmmelbas  21655  frlmelbas  21672  frlmphl  21697  islindf4  21754  rnascl  21807  psrlinv  21871  opsrbaslem  21963  evlseu  21997  mpfsubrg  22017  psdmvr  22063  ply1scl0OLD  22184  evl1sca  22228  evls1var  22232  matbas  22307  matplusg  22308  matsca  22309  matvsca  22310  matbas2d  22317  matsubgcell  22328  matmulcell  22339  ofco2  22345  mattposm  22353  mat1f1o  22372  mdetunilem8  22513  madugsum  22537  cramerimplem2  22578  decpmatmullem  22665  paste  23188  ptpjcn  23505  uptx  23519  xpstopnlem1  23703  alexsubALTlem4  23944  cnextf  23960  submtmd  23998  ussval  24154  tuslem  24161  psmetge0  24207  xmetge0  24239  setsmsds  24371  sgrim  24526  tnglem  24535  tngtset  24544  tngngp2  24547  resubmet  24697  pcorev2  24935  om1plusg  24941  om1tset  24942  om1opn  24943  pi1grplem  24956  clmadd  24981  clmmul  24982  clmcj  24983  tcphtopn  25133  tchnmfval  25135  bcthlem1  25231  bcthlem2  25232  bcthlem4  25234  bcth3  25238  rrxmval  25312  rrxmfval  25313  rrxdsfi  25318  ehlbase  25322  minveclem3b  25335  pjthlem1  25344  volun  25453  voliun  25462  uniioovol  25487  itg2i1fseq  25663  itgcnlem  25698  iblabslem  25736  limcres  25794  cnplimc  25795  ply1termlem  26115  0dgr  26157  taylthlem1  26288  abelth  26358  lawcos  26733  lgambdd  26954  basellem8  27005  musum  27108  chtub  27130  dchrval  27152  dchrinvcl  27171  lgsval4lem  27226  lgsquadlem2  27299  m1lgs  27306  cuteq0  27751  precsexlem11  28126  seqsval  28189  n0sbday  28251  zseo  28315  mirauto  28618  lmiisolem  28730  ttglem  28810  axlowdimlem16  28891  ebtwntg  28916  ecgrtg  28917  elntg2  28919  nbgrval  29270  uvtxupgrres  29342  clwlknf1oclwwlknlem3  30019  eucrct2eupth  30181  smcnlem  30633  siii  30789  pjhthlem1  31327  sbcies  32424  imadifxp  32537  dfimafnf  32567  funcnvmpt  32598  ccatws1f1olast  32881  gsumwun  33012  symgcom  33047  cycpmconjslem1  33118  rloc0g  33229  rloc1r  33230  resvlem  33312  qusker  33327  elrspunsn  33407  opprqusplusg  33467  idlsrgbas  33482  idlsrgplusg  33483  idlsrgmulr  33485  idlsrgtset  33486  idlsrgmulrval  33487  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  irredminply  33713  algextdeglem4  33717  algextdeglem5  33718  constrrtcc  33732  cos9thpinconstrlem1  33786  mdetpmtr12  33822  zarcls  33871  zar0ring  33875  pstmval  33892  xpinpreima2  33904  pnfneige0  33948  zlmds  33959  zlmtset  33960  esumid  34041  esumrnmpt  34049  sxsigon  34189  carsgclctunlem1  34315  circlemethnat  34639  fnrelpredd  35086  f1resfz0f1d  35108  pthhashvtx  35122  filnetlem4  36376  setsstrset  37131  finxpreclem4  37389  itg2addnclem  37672  iblabsnclem  37684  areacirc  37714  fnopabco  37724  heiborlem8  37819  rngoi  37900  drngoi  37952  ldualvsub  39155  dalemrotyz  39659  dalem6  39669  dalem7  39670  dalem11  39675  dalem12  39676  dalemrotps  39692  dalem30  39703  dalem35  39708  cdleme1  40228  cdleme9  40254  cdleme20c  40312  cdleme20d  40313  cdlemefrs29clN  40400  cdleme37m  40463  cdleme43aN  40490  cdlemg1b2  40572  cdlemg4f  40616  cdlemh2  40817  erngdvlem1  40989  erngdvlem2N  40990  erngdvlem3  40991  erngdvlem4  40992  erngdvlem1-rN  40997  erngdvlem2-rN  40998  erngdvlem3-rN  40999  erngdvlem4-rN  41000  dvh4dimN  41448  lcdvsub  41618  hlhilsca  41936  hlhilbase  41937  hlhilplus  41938  hlhilvsca  41948  hlhilip  41949  hlhilipval  41950  reelznn0nn  42456  rnasclg  42494  evlsval3  42554  prjspeclsp  42607  mzpcompact2lem  42746  eldioph2lem1  42755  fiphp3d  42814  rmxypairf1o  42907  wopprc  43026  lmhmlnmsplit  43083  rp-tfslim  43349  onsucunitp  43369  clcnvlem  43619  mnringnmulrd  44210  mnringbaserd  44212  mnringmulrd  44219  dmmptdff  45224  dmmptdf2  45234  ellimcabssub0  45622  cosknegpi  45874  dvnprodlem1  45951  fourierdlem58  46169  fourierdlem59  46170  fourierdlem72  46183  fourierdlem80  46191  sqwvfourb  46234  etransclem28  46267  etransclem41  46280  omef  46501  dfaimafn  47170  afv2co2  47262  sbgoldbo  47792  rrxlinesc  48728  rrxlinec  48729  rrx2linest2  48737  rrxsphere  48741  itsclinecirc0b  48767  itsclquadb  48769  2oppf  49125  idfullsubc  49154  oppc1stf  49281  oppc2ndf  49282  dfinito4  49494  prstcnid  49546  prstcthin  49554