Theorem eqtr3di 2815

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3di.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3di	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 ⊢ 𝐴 = 𝐶
2	1	eqcomi 2774	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2813	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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  resdmdfsnOLD  6034  f0dom0  6766  f1o00  6860  fmpt  7109  fmptsn  7171  fninfp  7178  uniordint  7806  fsuppeq  8177  fsuppeqg  8178  mapsnd  8890  sbthlem4  9085  sbthlem6  9087  findcard2s  9157  ssfi  9164  elfiun  9397  cnfcom2  9678  rankxplim3  9860  rankxpsuc  9861  pm54.43  10003  axdc3lem4  10452  gruun  10806  recmulnq  10964  reclem3pr  11049  xrmineq  13222  xadddi2  13339  iooval2  13421  hashsng  14423  hashfun  14492  hashbc  14508  swrds2m  15002  isumclim3  15833  isummulc2  15836  iprodclim3  16077  bpolydiflem  16130  bpoly4  16135  fprodefsum  16171  ruclem4  16312  bitsshft  16555  phimullem  16860  pythagtriplem1  16898  1arithlem4  17008  fsets  17251  topnid  17510  submefmnd  18991  pgrpsubgsymg  19523  odhash  19688  gsumzf1o  20026  gsumdifsnd  20075  pgpfaclem1  20197  fincygsubgodd  20228  subdrgint  20956  mplcoe1  22238  mplcoe5  22241  evlslem4  22277  selvvvval  22343  ordtrest2  23411  ufildr  24139  tsmsres  24352  zlmclm  25322  cphipval2  25451  csschl  25586  rrxcph  25602  volinun  25756  uniioombllem4  25796  itg1climres  25924  limcco  26103  vieta1lem2  26523  coseq00topi  26718  tangtx  26721  coskpi  26739  advlog  26870  advlogexp  26871  logtayl  26876  logccv  26879  dvcxp1  26956  dvcncxp1  26959  loglesqrt  26977  ang180lem3  27027  dquart  27069  atans2  27147  basellem8  27303  chtub  27427  bposlem6  27504  lgsquadlem2  27596  logdivsum  27748  log2sumbnd  27759  nodenselem5  27903  oldsuc  28130  precsexlem3  28453  spthispth  30136  ipval3  31132  siii  31276  cm2j  32043  pjssmii  32104  opsqrlem1  32563  hmopidmchi  32574  hmopidmpji  32575  pjcmul1i  32624  mddmd2  32732  cvexchlem  32791  dmdbr6ati  32846  difeq  32935  difuncomp  32969  ffsrn  33143  fzo0opth  33218  symgcom2  33468  cycpmcl  33500  cycpm2tr  33503  rhmimaidl  33804  drngidlhash  33805  1arithidomlem2  33890  qusdimsum  34082  2sqr3minply  34234  cos9thpiminplylem2  34237  zarcmplem  34335  ordtprsuni  34373  ordtrest2NEW  34377  zzsnm  34413  measun  34666  sxbrsigalem2  34741  carsgsigalem  34770  eulerpartlemgu  34832  gsumnunsn  34996  signsplypnf  35002  logdivsqrle  35102  cvmlift2lem12  35843  satf0suc  35905  nepss  36247  fwddifnp1  36694  finxpreclem1  38092  finxpreclem3  38096  poimirlem3  38331  poimirlem31  38359  ismblfin  38369  dvtan  38378  itg2addnclem3  38381  dvasin  38412  dvacos  38413  dvreasin  38414  dvreacos  38415  areacirclem1  38416  cnvepima  39044  disjimeceqim  39511  glbconN  40209  pmodl42N  40683  2polssN  40747  cdleme20j  41150  trlcocnv  41552  trlcone  41560  lclkrlem2c  42341  readvrec2  43180  sn-00idlem3  43219  sn-mul01  43245  diophrw  43548  wopprc  43815  onuniintrab  44011  fsovcnvlem  44797  sineq0ALT  45703  founiiun0  45966  iccdifioo  46289  itgvol0  46740  fourierdlem33  46912  etransclem32  47038  simpcntrab  47642  chnsubseqwl  47653  sin5tlem1  47668  cycl3grtrilem  48769  gpg3kgrtriexlem2  48907  gpgprismgr4cycllem3  48920  gsumdifsndf  49003  zlmodzxzadd  49195  cosn  49669  oppcendc  49853  resccatlem  49908  resccat  49909  0funcg2  49919  imaf1hom  49943