MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr3di Structured version   Visualization version   GIF version

Theorem eqtr3di 2792
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
StepHypRef Expression
1 eqtr3di.2 . . 3 𝐴 = 𝐶
21eqcomi 2746 . 2 𝐶 = 𝐴
3 eqtr3di.1 . 2 (𝜑𝐴 = 𝐵)
42, 3eqtr2id 2790 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729
This theorem is referenced by:  resdmdfsn  5992  f0dom0  6731  f1o00  6824  fmpt  7063  fmptsn  7118  fninfp  7125  uniordint  7741  fsuppeq  8111  fsuppeqg  8112  mapsnd  8831  sbthlem4  9037  sbthlem6  9039  findcard2s  9116  ssfi  9124  elfiun  9373  cnfcom2  9645  rankxplim3  9824  rankxpsuc  9825  pm54.43  9944  axdc3lem4  10396  gruun  10749  recmulnq  10907  reclem3pr  10992  xrmineq  13106  xadddi2  13223  iooval2  13304  hashsng  14276  hashfun  14344  hashbc  14357  swrds2m  14837  isumclim3  15651  isummulc2  15654  iprodclim3  15890  bpolydiflem  15944  bpoly4  15949  fprodefsum  15984  ruclem4  16123  bitsshft  16362  phimullem  16658  pythagtriplem1  16695  1arithlem4  16805  fsets  17048  topnid  17324  submefmnd  18712  pgrpsubgsymg  19198  odhash  19363  gsumzf1o  19696  gsumdifsnd  19745  pgpfaclem1  19867  fincygsubgodd  19898  subdrgint  20286  mplcoe1  21454  mplcoe5  21457  evlslem4  21500  ordtrest2  22571  ufildr  23298  tsmsres  23511  zlmclm  24491  cphipval2  24621  csschl  24756  rrxcph  24772  volinun  24926  uniioombllem4  24966  itg1climres  25095  limcco  25273  vieta1lem2  25687  coseq00topi  25875  tangtx  25878  coskpi  25895  advlog  26025  advlogexp  26026  logtayl  26031  logccv  26034  dvcxp1  26109  dvcncxp1  26112  loglesqrt  26127  ang180lem3  26177  dquart  26219  atans2  26297  basellem8  26453  chtub  26576  bposlem6  26653  lgsquadlem2  26745  logdivsum  26897  log2sumbnd  26908  nodenselem5  27052  oldsuc  27237  spthispth  28716  ipval3  29693  siii  29837  cm2j  30604  pjssmii  30665  opsqrlem1  31124  hmopidmchi  31135  hmopidmpji  31136  pjcmul1i  31185  mddmd2  31293  cvexchlem  31352  dmdbr6ati  31407  difeq  31487  difuncomp  31514  ffsrn  31688  symgcom2  31977  cycpmcl  32007  cycpm2tr  32010  rhmimaidl  32246  qusdimsum  32363  zarcmplem  32502  ordtprsuni  32540  ordtrest2NEW  32544  zzsnm  32580  measun  32850  sxbrsigalem2  32926  carsgsigalem  32955  eulerpartlemgu  33017  gsumnunsn  33193  signsplypnf  33202  logdivsqrle  33303  cvmlift2lem12  33948  satf0suc  34010  nepss  34329  fwddifnp1  34779  finxpreclem1  35889  finxpreclem3  35893  poimirlem31  36138  ismblfin  36148  dvtan  36157  itg2addnclem3  36160  dvasin  36191  dvacos  36192  dvreasin  36193  dvreacos  36194  areacirclem1  36195  cnvepima  36827  glbconN  37868  glbconNOLD  37869  pmodl42N  38343  2polssN  38407  cdleme20j  38810  trlcocnv  39212  trlcone  39220  lclkrlem2c  40001  sn-mul01  40923  diophrw  41111  wopprc  41383  onuniintrab  41589  fsovcnvlem  42359  sineq0ALT  43293  founiiun0  43483  iccdifioo  43827  itgvol0  44283  fourierdlem33  44455  etransclem32  44581  simpcntrab  45185  gsumdifsndf  46189  zlmodzxzadd  46508
  Copyright terms: Public domain W3C validator