Theorem eqtr3di 2811

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 2770	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2809	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 2155  ax-ext 2733

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

This theorem is used by:  resdmdfsnOLD  6022  f0dom0  6764  f1o00  6858  fmpt  7108  fmptsn  7170  fninfp  7177  uniordint  7813  fsuppeq  8185  fsuppeqg  8186  mapsnd  8907  sbthlem4  9102  sbthlem6  9104  findcard2s  9174  ssfi  9181  elfiun  9415  cnfcom2  9696  rankxplim3  9891  rankxpsuc  9892  pm54.43  10075  axdc3lem4  10524  gruun  10884  recmulnq  11042  reclem3pr  11127  xrmineq  13303  xadddi2  13420  iooval2  13502  hashsng  14506  hashfun  14575  hashbc  14591  swrds2m  15085  isumclim3  15918  isummulc2  15921  iprodclim3  16160  bpolydiflem  16213  bpoly4  16218  fprodefsum  16254  ruclem4  16395  bitsshft  16638  phimullem  16949  pythagtriplem1  16987  1arithlem4  17097  fsets  17340  topnid  17599  submefmnd  19084  pgrpsubgsymg  19616  odhash  19781  gsumzf1o  20119  gsumdifsnd  20168  pgpfaclem1  20290  fincygsubgodd  20321  subdrgint  21053  mplcoe1  22339  mplcoe5  22342  evlslem4  22378  selvvvval  22444  ordtrest2  23515  ufildr  24243  tsmsres  24456  zlmclm  25426  cphipval2  25555  csschl  25690  rrxcph  25706  volinun  25860  uniioombllem4  25900  itg1climres  26028  limcco  26206  rnplynfin  26623  vieta1lem2  26627  coseq00topi  26824  tangtx  26827  coskpi  26844  advlog  26975  advlogexp  26976  logtayl  26981  logccv  26984  dvcxp1  27061  dvcncxp1  27064  loglesqrt  27082  ang180lem3  27132  dquart  27174  atans2  27252  basellem8  27408  chtub  27532  bposlem6  27609  lgsquadlem2  27701  logdivsum  27853  log2sumbnd  27864  nodenselem5  28038  oldsuc  28265  precsexlem3  28588  spthispth  30302  ipval3  31304  siii  31448  cm2j  32215  pjssmii  32276  opsqrlem1  32735  hmopidmchi  32746  hmopidmpji  32747  pjcmul1i  32796  mddmd2  32904  cvexchlem  32963  dmdbr6ati  33018  difeq  33107  difuncomp  33141  ffsrn  33313  fzo0opth  33388  symgcom2  33638  cycpmcl  33670  cycpm2tr  33673  rhmimaidl  33975  drngidlhash  33976  1arithidomlem2  34061  qusdimsum  34253  2sqr3minply  34405  cos9thpiminplylem2  34408  zarcmplem  34506  ordtprsuni  34544  ordtrest2NEW  34548  zzsnm  34584  measun  34837  sxbrsigalem2  34911  carsgsigalem  34940  eulerpartlemgu  35002  gsumnunsn  35166  signsplypnf  35172  logdivsqrle  35272  cvmlift2lem12  36058  satf0suc  36120  nepss  36462  fwddifnp1  36910  finxpreclem1  38292  finxpreclem3  38296  poimirlem3  38521  poimirlem31  38549  ismblfin  38559  dvtan  38568  itg2addnclem3  38571  dvasin  38602  dvacos  38603  dvreasin  38604  dvreacos  38605  areacirclem1  38606  cnvepima  39249  disjimeceqim  39716  glbconN  40414  pmodl42N  40888  2polssN  40952  cdleme20j  41355  trlcocnv  41757  trlcone  41765  lclkrlem2c  42546  readvrec2  43392  sn-00idlem3  43431  sn-mul01  43457  diophrw  43749  wopprc  44016  onuniintrab  44212  fsovcnvlem  44998  sineq0ALT  45904  founiiun0  46174  iccdifioo  46496  itgvol0  46947  fourierdlem33  47119  etransclem32  47245  simpcntrab  47849  chnsubseqwl  47858  sin5tlem1  47888  cycl3grtrilem  49013  gpg3kgrtriexlem2  49151  gpgprismgr4cycllem3  49164  gsumdifsndf  49247  zlmodzxzadd  49439  cosn  49913  oppcendc  50095  resccatlem  50150  resccat  50151  0funcg2  50161  imaf1hom  50185