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 ⊢ (𝜑 → 𝐵 = 𝐶)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  resdmdfsnOLD  6032  f0dom0  6762  f1o00  6856  fmpt  7105  fmptsn  7165  fninfp  7172  uniordint  7796  fsuppeq  8167  fsuppeqg  8168  mapsnd  8880  sbthlem4  9074  sbthlem6  9076  findcard2s  9146  ssfi  9153  elfiun  9386  cnfcom2  9667  rankxplim3  9849  rankxpsuc  9850  pm54.43  9983  axdc3lem4  10432  gruun  10786  recmulnq  10944  reclem3pr  11029  xrmineq  13201  xadddi2  13318  iooval2  13400  hashsng  14401  hashfun  14470  hashbc  14486  swrds2m  14974  isumclim3  15806  isummulc2  15809  iprodclim3  16050  bpolydiflem  16103  bpoly4  16108  fprodefsum  16144  ruclem4  16285  bitsshft  16528  phimullem  16833  pythagtriplem1  16871  1arithlem4  16981  fsets  17224  topnid  17483  submefmnd  18949  pgrpsubgsymg  19474  odhash  19639  gsumzf1o  19977  gsumdifsnd  20026  pgpfaclem1  20148  fincygsubgodd  20179  subdrgint  20906  mplcoe1  22188  mplcoe5  22191  evlslem4  22227  selvvvval  22293  ordtrest2  23361  ufildr  24088  tsmsres  24301  zlmclm  25271  cphipval2  25400  csschl  25535  rrxcph  25551  volinun  25705  uniioombllem4  25745  itg1climres  25873  limcco  26052  vieta1lem2  26472  coseq00topi  26667  tangtx  26670  coskpi  26688  advlog  26819  advlogexp  26820  logtayl  26825  logccv  26828  dvcxp1  26905  dvcncxp1  26908  loglesqrt  26926  ang180lem3  26976  dquart  27018  atans2  27096  basellem8  27252  chtub  27376  bposlem6  27453  lgsquadlem2  27545  logdivsum  27697  log2sumbnd  27708  nodenselem5  27852  oldsuc  28079  precsexlem3  28402  spthispth  30073  ipval3  31061  siii  31205  cm2j  31972  pjssmii  32033  opsqrlem1  32492  hmopidmchi  32503  hmopidmpji  32504  pjcmul1i  32553  mddmd2  32661  cvexchlem  32720  dmdbr6ati  32775  difeq  32864  difuncomp  32898  ffsrn  33073  fzo0opth  33148  symgcom2  33404  cycpmcl  33436  cycpm2tr  33439  rhmimaidl  33740  drngidlhash  33741  1arithidomlem2  33826  qusdimsum  34018  2sqr3minply  34170  cos9thpiminplylem2  34173  zarcmplem  34271  ordtprsuni  34309  ordtrest2NEW  34313  zzsnm  34349  measun  34601  sxbrsigalem2  34676  carsgsigalem  34705  eulerpartlemgu  34767  gsumnunsn  34931  signsplypnf  34937  logdivsqrle  35037  cvmlift2lem12  35806  satf0suc  35868  nepss  36210  fwddifnp1  36657  finxpreclem1  38035  finxpreclem3  38039  poimirlem3  38274  poimirlem31  38302  ismblfin  38312  dvtan  38321  itg2addnclem3  38324  dvasin  38355  dvacos  38356  dvreasin  38357  dvreacos  38358  areacirclem1  38359  cnvepima  38986  disjimeceqim  39453  glbconN  40151  pmodl42N  40625  2polssN  40689  cdleme20j  41092  trlcocnv  41494  trlcone  41502  lclkrlem2c  42283  readvrec2  43122  sn-00idlem3  43161  sn-mul01  43187  diophrw  43490  wopprc  43757  onuniintrab  43953  fsovcnvlem  44739  sineq0ALT  45645  founiiun0  45908  iccdifioo  46231  itgvol0  46682  fourierdlem33  46854  etransclem32  46980  simpcntrab  47584  chnsubseqwl  47595  sin5tlem1  47610  cycl3grtrilem  48711  gpg3kgrtriexlem2  48849  gpgprismgr4cycllem3  48862  gsumdifsndf  48946  zlmodzxzadd  49138  cosn  49612  oppcendc  49796  resccatlem  49851  resccat  49852  0funcg2  49862  imaf1hom  49886