Theorem eqtr3di 2810

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 2769	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2808	1 ⊢ (𝜑 → 𝐵 = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  resdmdfsnOLD  6024  f0dom0  6771  f1o00  6865  fmpt  7115  fmptsn  7176  fninfp  7183  uniordint  7819  fsuppeq  8199  fsuppeqg  8200  mapsnd  8921  sbthlem4  9116  sbthlem6  9118  findcard2s  9188  ssfi  9195  elfiun  9429  cnfcom2  9710  rankxplim3  9905  rankxpsuc  9906  pm54.43  10089  axdc3lem4  10538  gruun  10898  recmulnq  11056  reclem3pr  11141  xrmineq  13317  xadddi2  13434  iooval2  13516  hashsng  14520  hashfun  14589  hashbc  14605  swrds2m  15101  isumclim3  15934  isummulc2  15937  iprodclim3  16176  bpolydiflem  16229  bpoly4  16234  fprodefsum  16270  ruclem4  16411  bitsshft  16654  phimullem  16965  pythagtriplem1  17003  1arithlem4  17113  fsets  17356  topnid  17615  submefmnd  19100  pgrpsubgsymg  19632  odhash  19797  gsumzf1o  20135  gsumdifsnd  20184  pgpfaclem1  20306  fincygsubgodd  20337  subdrgint  21069  mplcoe1  22355  mplcoe5  22358  evlslem4  22394  selvvvval  22460  ordtrest2  23531  ufildr  24259  tsmsres  24472  zlmclm  25442  cphipval2  25571  csschl  25706  rrxcph  25722  volinun  25876  uniioombllem4  25916  itg1climres  26044  limcco  26222  rnplynfin  26639  vieta1lem2  26643  coseq00topi  26840  tangtx  26843  coskpi  26860  advlog  26991  advlogexp  26992  logtayl  26997  logccv  27000  dvcxp1  27077  dvcncxp1  27080  loglesqrt  27098  ang180lem3  27148  dquart  27190  atans2  27268  basellem8  27424  chtub  27548  bposlem6  27625  lgsquadlem2  27717  logdivsum  27869  log2sumbnd  27880  nodenselem5  28054  oldsuc  28281  precsexlem3  28604  spthispth  30318  ipval3  31320  siii  31464  cm2j  32231  pjssmii  32292  opsqrlem1  32751  hmopidmchi  32762  hmopidmpji  32763  pjcmul1i  32812  mddmd2  32920  cvexchlem  32979  dmdbr6ati  33034  difeq  33165  difuncomp  33199  ffsrn  33370  fzo0opth  33445  symgcom2  33695  cycpmcl  33727  cycpm2tr  33730  rhmimaidl  34032  drngidlhash  34033  1arithidomlem2  34118  qusdimsum  34310  2sqr3minply  34462  cos9thpiminplylem2  34465  zarcmplem  34563  ordtprsuni  34601  ordtrest2NEW  34605  zzsnm  34641  measun  34894  sxbrsigalem2  34968  carsgsigalem  34997  eulerpartlemgu  35059  gsumnunsn  35223  signsplypnf  35229  logdivsqrle  35329  cvmlift2lem12  36169  satf0suc  36231  nepss  36579  fwddifnp1  37026  finxpreclem1  38421  finxpreclem3  38425  poimirlem3  38650  poimirlem31  38678  ismblfin  38688  dvtan  38697  itg2addnclem3  38700  dvasin  38731  dvacos  38732  dvreasin  38733  dvreacos  38734  areacirclem1  38735  cnvepima  39378  disjimeceqim  39845  glbconN  40543  pmodl42N  41017  2polssN  41081  cdleme20j  41484  trlcocnv  41886  trlcone  41894  lclkrlem2c  42675  readvrec2  43521  sn-00idlem3  43560  sn-mul01  43586  diophrw  43879  wopprc  44146  onuniintrab  44337  fsovcnvlem  45122  sineq0ALT  46027  founiiun0  46313  iccdifioo  46635  itgvol0  47086  fourierdlem33  47258  etransclem32  47384  simpcntrab  47988  chnsubseqwl  47997  sin5tlem1  48027  cycl3grtrilem  49152  gpg3kgrtriexlem2  49290  gpgprismgr4cycllem3  49303  gsumdifsndf  49386  zlmodzxzadd  49578  cosn  50053  oppcendc  50240  resccatlem  50295  resccat  50296  0funcg2  50307  imaf1hom  50332