Theorem eqtr3di 2794

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  resdmdfsn  5944  f0dom0  6667  f1o00  6760  fmpt  6993  fmptsn  7048  fninfp  7055  uniordint  7660  frnsuppeq  8000  frnsuppeqg  8001  mapsnd  8683  sbthlem4  8882  sbthlem6  8884  findcard2s  8957  ssfi  8965  elfiun  9198  cnfcom2  9469  rankxplim3  9648  rankxpsuc  9649  pm54.43  9768  axdc3lem4  10218  gruun  10571  recmulnq  10729  reclem3pr  10814  xrmineq  12923  xadddi2  13040  iooval2  13121  hashsng  14093  hashfun  14161  hashbc  14174  swrds2m  14663  isumclim3  15480  isummulc2  15483  iprodclim3  15719  bpolydiflem  15773  bpoly4  15778  fprodefsum  15813  ruclem4  15952  bitsshft  16191  phimullem  16489  pythagtriplem1  16526  1arithlem4  16636  fsets  16879  topnid  17155  submefmnd  18543  pgrpsubgsymg  19026  odhash  19188  gsumzf1o  19522  gsumdifsnd  19571  pgpfaclem1  19693  fincygsubgodd  19724  subdrgint  20080  mplcoe1  21247  mplcoe5  21250  evlslem4  21293  ordtrest2  22364  ufildr  23091  tsmsres  23304  zlmclm  24284  cphipval2  24414  csschl  24549  rrxcph  24565  volinun  24719  uniioombllem4  24759  itg1climres  24888  limcco  25066  vieta1lem2  25480  coseq00topi  25668  tangtx  25671  coskpi  25688  advlog  25818  advlogexp  25819  logtayl  25824  logccv  25827  dvcxp1  25902  dvcncxp1  25905  loglesqrt  25920  ang180lem3  25970  dquart  26012  atans2  26090  basellem8  26246  chtub  26369  bposlem6  26446  lgsquadlem2  26538  logdivsum  26690  log2sumbnd  26701  spthispth  28103  ipval3  29080  siii  29224  cm2j  29991  pjssmii  30052  opsqrlem1  30511  hmopidmchi  30522  hmopidmpji  30523  pjcmul1i  30572  mddmd2  30680  cvexchlem  30739  dmdbr6ati  30794  difeq  30874  difuncomp  30902  ffsrn  31073  symgcom2  31362  cycpmcl  31392  cycpm2tr  31395  rhmimaidl  31618  qusdimsum  31718  zarcmplem  31840  ordtprsuni  31878  ordtrest2NEW  31882  zzsnm  31918  measun  32188  sxbrsigalem2  32262  carsgsigalem  32291  eulerpartlemgu  32353  gsumnunsn  32529  signsplypnf  32538  logdivsqrle  32639  cvmlift2lem12  33285  satf0suc  33347  nepss  33671  nodenselem5  33900  oldsuc  34077  fwddifnp1  34476  finxpreclem1  35569  finxpreclem3  35573  poimirlem31  35817  ismblfin  35827  dvtan  35836  itg2addnclem3  35839  dvasin  35870  dvacos  35871  dvreasin  35872  dvreacos  35873  areacirclem1  35874  cnvepima  36479  glbconN  37398  pmodl42N  37872  2polssN  37936  cdleme20j  38339  trlcocnv  38741  trlcone  38749  lclkrlem2c  39530  sn-mul01  40414  diophrw  40588  wopprc  40859  fsovcnvlem  41628  sineq0ALT  42564  founiiun0  42735  iccdifioo  43060  itgvol0  43516  fourierdlem33  43688  etransclem32  43814  simpcntrab  44397  gsumdifsndf  45386  zlmodzxzadd  45705