Theorem eqtr3di 2786

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 2740	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2784	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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  resdmdfsn  6031  f0dom0  6775  f1o00  6868  fmpt  7111  fmptsn  7167  fninfp  7174  uniordint  7793  fsuppeq  8165  fsuppeqg  8166  mapsnd  8886  sbthlem4  9092  sbthlem6  9094  findcard2s  9171  ssfi  9179  elfiun  9431  cnfcom2  9703  rankxplim3  9882  rankxpsuc  9883  pm54.43  10002  axdc3lem4  10454  gruun  10807  recmulnq  10965  reclem3pr  11050  xrmineq  13166  xadddi2  13283  iooval2  13364  hashsng  14336  hashfun  14404  hashbc  14419  swrds2m  14899  isumclim3  15712  isummulc2  15715  iprodclim3  15951  bpolydiflem  16005  bpoly4  16010  fprodefsum  16045  ruclem4  16184  bitsshft  16423  phimullem  16719  pythagtriplem1  16756  1arithlem4  16866  fsets  17109  topnid  17388  submefmnd  18815  pgrpsubgsymg  19322  odhash  19487  gsumzf1o  19825  gsumdifsnd  19874  pgpfaclem1  19996  fincygsubgodd  20027  subdrgint  20566  mplcoe1  21816  mplcoe5  21819  evlslem4  21861  ordtrest2  22941  ufildr  23668  tsmsres  23881  zlmclm  24872  cphipval2  25002  csschl  25137  rrxcph  25153  volinun  25308  uniioombllem4  25348  itg1climres  25477  limcco  25655  vieta1lem2  26074  coseq00topi  26263  tangtx  26266  coskpi  26283  advlog  26413  advlogexp  26414  logtayl  26419  logccv  26422  dvcxp1  26499  dvcncxp1  26502  loglesqrt  26517  ang180lem3  26567  dquart  26609  atans2  26687  basellem8  26843  chtub  26966  bposlem6  27043  lgsquadlem2  27135  logdivsum  27287  log2sumbnd  27298  nodenselem5  27442  oldsuc  27632  precsexlem3  27909  spthispth  29265  ipval3  30244  siii  30388  cm2j  31155  pjssmii  31216  opsqrlem1  31675  hmopidmchi  31686  hmopidmpji  31687  pjcmul1i  31736  mddmd2  31844  cvexchlem  31903  dmdbr6ati  31958  difeq  32038  difuncomp  32067  ffsrn  32236  symgcom2  32530  cycpmcl  32560  cycpm2tr  32563  rhmimaidl  32839  drngidlhash  32841  qusdimsum  33016  zarcmplem  33174  ordtprsuni  33212  ordtrest2NEW  33216  zzsnm  33252  measun  33522  sxbrsigalem2  33598  carsgsigalem  33627  eulerpartlemgu  33689  gsumnunsn  33865  signsplypnf  33874  logdivsqrle  33975  cvmlift2lem12  34618  satf0suc  34680  nepss  35006  fwddifnp1  35456  finxpreclem1  36586  finxpreclem3  36590  poimirlem31  36835  ismblfin  36845  dvtan  36854  itg2addnclem3  36857  dvasin  36888  dvacos  36889  dvreasin  36890  dvreacos  36891  areacirclem1  36892  cnvepima  37522  glbconN  38563  glbconNOLD  38564  pmodl42N  39038  2polssN  39102  cdleme20j  39505  trlcocnv  39907  trlcone  39915  lclkrlem2c  40696  selvvvval  41472  sn-mul01  41613  diophrw  41812  wopprc  42084  onuniintrab  42290  fsovcnvlem  43079  sineq0ALT  44013  founiiun0  44200  iccdifioo  44539  itgvol0  44995  fourierdlem33  45167  etransclem32  45293  simpcntrab  45897  gsumdifsndf  46870  zlmodzxzadd  47135