Theorem eqtr3di 2813

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 2772	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2811	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  resdmdfsnOLD  6040  f0dom0  6796  f1o00  6891  fmpt  7142  fmptsn  7203  fninfp  7210  uniordint  7849  fsuppeq  8230  fsuppeqg  8231  mapsnd  8952  sbthlem4  9147  sbthlem6  9149  findcard2s  9219  ssfi  9226  elfiun  9459  cnfcom2  9740  rankxplim3  9935  rankxpsuc  9936  pm54.43  10121  axdc3lem4  10570  gruun  10930  recmulnq  11088  reclem3pr  11173  xrmineq  13350  xadddi2  13467  iooval2  13549  hashsng  14554  hashfun  14623  hashbc  14639  swrds2m  15135  isumclim3  15969  isummulc2  15972  iprodclim3  16211  bpolydiflem  16264  bpoly4  16269  fprodefsum  16305  ruclem4  16446  bitsshft  16689  phimullem  17000  pythagtriplem1  17038  1arithlem4  17148  fsets  17391  topnid  17656  submefmnd  19141  pgrpsubgsymg  19674  odhash  19839  gsumzf1o  20177  gsumdifsnd  20226  pgpfaclem1  20348  fincygsubgodd  20379  subdrgint  21111  mplcoe1  22401  mplcoe5  22404  evlslem4  22440  selvvvval  22506  ordtrest2  23577  ufildr  24305  tsmsres  24518  zlmclm  25488  cphipval2  25617  csschl  25752  rrxcph  25768  volinun  25922  uniioombllem4  25962  itg1climres  26090  limcco  26268  rnplynfin  26685  vieta1lem2  26689  coseq00topi  26888  tangtx  26891  coskpi  26908  advlog  27039  advlogexp  27040  logtayl  27045  logccv  27048  dvcxp1  27125  dvcncxp1  27128  loglesqrt  27146  ang180lem3  27196  dquart  27238  atans2  27316  basellem8  27472  chtub  27596  bposlem6  27673  lgsquadlem2  27765  logdivsum  27917  log2sumbnd  27928  nodenselem5  28102  oldsuc  28329  precsexlem3  28652  spthispth  30366  ipval3  31368  siii  31512  cm2j  32279  pjssmii  32340  opsqrlem1  32799  hmopidmchi  32810  hmopidmpji  32811  pjcmul1i  32860  mddmd2  32968  cvexchlem  33027  dmdbr6ati  33082  difeq  33213  difuncomp  33246  ffsrn  33416  fzo0opth  33491  symgcom2  33744  cycpmcl  33776  cycpm2tr  33779  rhmimaidl  34086  drngidlhash  34087  1arithidomlem2  34172  qusdimsum  34371  2sqr3minply  34523  cos9thpiminplylem2  34526  zarcmplem  34624  ordtprsuni  34662  ordtrest2NEW  34666  zzsnm  34702  measun  34955  sxbrsigalem2  35029  carsgsigalem  35058  eulerpartlemgu  35120  gsumnunsn  35284  signsplypnf  35290  logdivsqrle  35390  cvmlift2lem12  36287  satf0suc  36349  nepss  36698  fwddifnp1  37145  finxpreclem1  38580  finxpreclem3  38584  poimirlem3  38809  poimirlem31  38837  ismblfin  38847  dvtan  38856  itg2addnclem3  38859  dvasin  38890  dvacos  38891  dvreasin  38892  dvreacos  38893  areacirclem1  38894  cnvepima  39535  disjimeceqim  40002  glbconN  40700  pmodl42N  41174  2polssN  41238  cdleme20j  41641  trlcocnv  42043  trlcone  42051  lclkrlem2c  42832  readvrec2  43678  sn-00idlem3  43717  sn-mul01  43743  diophrw  44036  wopprc  44303  onuniintrab  44489  fsovcnvlem  45274  sineq0ALT  46179  founiiun0  46478  iccdifioo  46800  itgvol0  47251  fourierdlem33  47423  etransclem32  47549  simpcntrab  48153  chnsubseqwl  48162  sin5tlem1  48192  cycl3grtrilem  49317  gpg3kgrtriexlem2  49455  gpgprismgr4cycllem3  49468  gsumdifsndf  49551  zlmodzxzadd  49801  cosn  50276  oppcendc  50463  resccatlem  50518  resccat  50519  0funcg2  50530  imaf1hom  50555