ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr4d GIF version

Theorem 3eqtr4d 2160
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4d.1 (𝜑𝐴 = 𝐵)
3eqtr4d.2 (𝜑𝐶 = 𝐴)
3eqtr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3eqtr4d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2 (𝜑𝐶 = 𝐴)
2 3eqtr4d.3 . . 3 (𝜑𝐷 = 𝐵)
3 3eqtr4d.1 . . 3 (𝜑𝐴 = 𝐵)
42, 3eqtr4d 2153 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2153 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  fnsnfv  5448  fvco2  5458  resfunexg  5609  fcof1  5652  fliftfun  5665  caovdir2d  5915  caov32d  5919  caov31d  5921  caov4d  5923  caovlem2d  5931  caofcom  5973  cnvf1olem  6089  tfrlem1  6173  tfrlemisucaccv  6190  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  frecrdg  6273  oav2  6327  omv2  6329  omsuc  6336  nnmsucr  6352  ecovicom  6505  ecoviass  6507  ecovidi  6509  carden2bex  7013  addcompig  7105  addasspig  7106  mulcompig  7107  mulasspig  7108  distrpig  7109  addassnqg  7158  addnq0mo  7223  mulnq0mo  7224  nqnq0a  7230  nqnq0m  7231  distrnq0  7235  mulcomnq0  7236  addassnq0  7238  addcmpblnr  7515  mulcmpblnrlemg  7516  addsrmo  7519  mulsrmo  7520  ltsrprg  7523  recexgt0sr  7549  mulgt0sr  7554  mulextsr1lem  7556  addcnsrec  7618  mulcnsrec  7619  pitonnlem2  7623  recidpirqlemcalc  7633  axaddcom  7646  adddir  7725  mul32  7860  mul31  7861  add32  7889  add4  7891  sub32  7964  sub4  7975  subdir  8116  mulneg2  8126  mulreim  8334  apadd1  8338  apneg  8341  divassap  8418  divdirap  8425  divmul13ap  8443  divmul24ap  8444  divdiv32ap  8448  conjmulap  8457  zeo  9124  xaddcom  9612  xnegdi  9619  xaddass  9620  xaddass2  9621  xpncan  9622  xadd4d  9636  lincmb01cmp  9754  iccf1o  9755  flhalf  10043  modqvalp1  10084  modqdi  10133  modqsubdir  10134  frecuzrdgg  10157  seq3shft2  10214  seq3caopr3  10222  seq3caopr  10224  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3f1olemqsum  10241  seq3homo  10251  seqfeq3  10253  seq3distr  10254  expp1  10268  expnegap0  10269  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  sqneg  10320  sqdivap  10325  subsq2  10368  binom2  10371  facp1  10444  bcm1k  10474  bcp1n  10475  bcval5  10477  omgadd  10516  hashun  10519  hashxp  10540  shftfibg  10560  shftfib  10563  shftval  10565  2shfti  10571  seq3shft  10578  crre  10597  remim  10600  mulreap  10604  reneg  10608  readd  10609  remullem  10611  redivap  10614  imneg  10616  imadd  10617  imdivap  10621  cjcj  10623  cjadd  10624  cjmulrcl  10627  cjneg  10630  imval2  10634  resqrexlemcalc1  10754  absneg  10790  sqabsadd  10795  sqabssub  10796  absmul  10809  absresq  10818  absexp  10819  absexpzap  10820  bdtrilem  10978  xrmaxiflemcom  10986  xrmaxadd  10998  xrminrecl  11010  xrminadd  11012  serf0  11089  summodclem3  11117  fsum3  11124  isumss  11128  fisumss  11129  fsumadd  11143  isummulc1  11164  isumdivapc  11165  fsum2dlemstep  11171  fisumcom2  11175  fisum0diag2  11184  fsummulc2  11185  fsummulc1  11186  fsumdivapc  11187  fsumconst  11191  telfsumo  11203  fsumparts  11207  binomlem  11220  isumshft  11227  arisum2  11236  geolim  11248  geo2sum  11251  geo2lim  11253  cvgratnnlemseq  11263  cvgratz  11269  mertenslem2  11273  efcllemp  11291  efcj  11306  efexp  11315  resinval  11349  recosval  11350  cosneg  11361  efival  11366  sinadd  11370  cosadd  11371  addcos  11380  sin2t  11383  cos2t  11384  odd2np1lem  11496  oexpneg  11501  neggcd  11598  gcdabs2  11605  mulgcd  11631  mulgcdr  11633  gcddiv  11634  rplpwr  11642  eucalgval  11662  eucalginv  11664  eucalg  11667  neglcm  11683  lcmgcd  11686  mulgcddvds  11702  qredeu  11705  nn0gcdsq  11805  phimullem  11828  ennnfonelemp1  11846  setsabsd  11925  setscom  11926  tgdom  12168  txbasval  12363  cnmpt11  12379  cnmpt21  12387  setsmsbasg  12575  bdbl  12599  dvmulxxbr  12762  dvimulf  12766  dvcj  12769  dvfre  12770  dvrecap  12773  dvef  12783  sinperlem  12816  coshalfpip  12830  ptolemy  12832  tangtx  12846  nninfalllemn  13129  nninfsellemeqinf  13139  refeq  13150
  Copyright terms: Public domain W3C validator