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

Theorem 3eqtr4d 2220
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 2213 . 2 (𝜑𝐷 = 𝐴)
51, 4eqtr4d 2213 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  fnsnfv  5570  fvco2  5580  resfunexg  5732  fcof1  5777  fliftfun  5790  caovdir2d  6044  caov32d  6048  caov31d  6050  caov4d  6052  caovlem2d  6060  caofcom  6099  cnvf1olem  6218  tfrlem1  6302  tfrlemisucaccv  6319  tfr1onlemsucaccv  6335  tfrcllemsucaccv  6348  frecrdg  6402  oav2  6457  omv2  6459  omsuc  6466  nnmsucr  6482  ecovicom  6636  ecoviass  6638  ecovidi  6640  nnnninfeq  7119  nninfwlpoimlemg  7166  carden2bex  7181  addcompig  7306  addasspig  7307  mulcompig  7308  mulasspig  7309  distrpig  7310  addassnqg  7359  addnq0mo  7424  mulnq0mo  7425  nqnq0a  7431  nqnq0m  7432  distrnq0  7436  mulcomnq0  7437  addassnq0  7439  addcmpblnr  7716  mulcmpblnrlemg  7717  addsrmo  7720  mulsrmo  7721  ltsrprg  7724  recexgt0sr  7750  mulgt0sr  7755  mulextsr1lem  7757  addcnsrec  7819  mulcnsrec  7820  pitonnlem2  7824  recidpirqlemcalc  7834  axaddcom  7847  adddir  7926  mul32  8064  mul31  8065  add32  8093  add4  8095  sub32  8168  sub4  8179  subdir  8320  mulneg2  8330  mulreim  8538  apadd1  8542  apneg  8545  divassap  8623  divdirap  8630  divmul13ap  8648  divmul24ap  8649  divdiv32ap  8653  conjmulap  8662  zeo  9334  xaddcom  9835  xnegdi  9842  xaddass  9843  xaddass2  9844  xpncan  9845  xadd4d  9859  lincmb01cmp  9977  iccf1o  9978  flhalf  10275  modqvalp1  10316  modqdi  10365  modqsubdir  10366  frecuzrdgg  10389  seq3shft2  10446  seq3caopr3  10454  seq3caopr  10456  seq3f1olemqsumkj  10471  seq3f1olemqsumk  10472  seq3f1olemqsum  10473  seq3homo  10483  seqfeq3  10485  seq3distr  10486  expp1  10500  expnegap0  10501  expaddzaplem  10536  expaddzap  10537  expmulzap  10539  sqneg  10552  sqdivap  10557  subsq2  10600  binom2  10604  modqexp  10619  facp1  10681  bcm1k  10711  bcp1n  10712  bcval5  10714  omgadd  10753  hashun  10756  hashxp  10777  shftfibg  10800  shftfib  10803  shftval  10805  2shfti  10811  seq3shft  10818  crre  10837  remim  10840  mulreap  10844  reneg  10848  readd  10849  remullem  10851  redivap  10854  imneg  10856  imadd  10857  imdivap  10861  cjcj  10863  cjadd  10864  cjmulrcl  10867  cjneg  10870  imval2  10874  resqrexlemcalc1  10994  absneg  11030  sqabsadd  11035  sqabssub  11036  absmul  11049  absresq  11058  absexp  11059  absexpzap  11060  bdtrilem  11218  xrmaxiflemcom  11228  xrmaxadd  11240  xrminrecl  11252  xrminadd  11254  serf0  11331  summodclem3  11359  fsum3  11366  isumss  11370  fisumss  11371  fsumadd  11385  isummulc1  11406  isumdivapc  11407  fsum2dlemstep  11413  fisumcom2  11417  fisum0diag2  11426  fsummulc2  11427  fsummulc1  11428  fsumdivapc  11429  fsumconst  11433  telfsumo  11445  fsumparts  11449  binomlem  11462  isumshft  11469  arisum2  11478  geolim  11490  geo2sum  11493  geo2lim  11495  cvgratnnlemseq  11505  cvgratz  11511  mertenslem2  11515  prodfrecap  11525  prodfdivap  11526  prodmodclem2a  11555  fprodntrivap  11563  fprodssdc  11569  fprodmul  11570  fprodabs  11595  fprod2dlemstep  11601  fprodcom2fi  11605  fprodrec  11608  efcllemp  11637  efcj  11652  efexp  11661  resinval  11694  recosval  11695  cosneg  11706  efival  11711  sinadd  11715  cosadd  11716  addcos  11725  sin2t  11728  cos2t  11729  dvdsmodexp  11773  odd2np1lem  11847  oexpneg  11852  neggcd  11954  gcdabs2  11961  mulgcd  11987  mulgcdr  11989  gcddiv  11990  rplpwr  11998  eucalgval  12024  eucalginv  12026  eucalg  12029  neglcm  12045  lcmgcd  12048  mulgcddvds  12064  qredeu  12067  nn0gcdsq  12170  phimullem  12195  prmdiv  12205  coprimeprodsq  12227  pythagtriplem1  12235  pythagtriplem3  12237  pythagtriplem4  12238  pythagtriplem12  12245  pceulem  12264  pceu  12265  pcqmul  12273  pcexp  12279  pcneg  12294  pcadd  12309  pcmpt  12311  pcmpt2  12312  pcbc  12319  4sqlem7  12352  4sqlem10  12355  mul4sqlem  12361  ennnfonelemp1  12377  setsabsd  12471  setscom  12472  ressbasd  12496  strressid  12499  ressinbasd  12502  ressressg  12503  ressplusgd  12553  grpidpropdg  12672  mnd32g  12707  mnd4g  12709  0mhm  12750  mhmco  12751  grpinvcnv  12814  grpinvpropdg  12821  grpinvsub  12828  grpaddsubass  12836  grpsubpropdg  12850  grpsubpropd2  12851  mulgnnp1  12867  mulgnegnn  12869  mulgaddcom  12882  mulginvcom  12883  mulgnndir  12887  mulgnn0ass  12894  mhmmulg  12899  mulgpropdg  12900  ablsub4  12930  ablsub32  12939  dfur2g  12958  srgass  12967  srgmulgass  12985  srgpcomp  12986  srglmhm  12989  srgrmhm  12990  crngcom  13010  ringass  13012  ringcom  13027  ringsubdi  13046  rngsubdir  13047  mulgass2  13048  opprring  13061  oppr0g  13063  oppr1g  13064  opprnegg  13065  mulgass3  13066  dvdsrvald  13074  unitlinv  13107  unitrinv  13108  tgdom  13205  txbasval  13400  cnmpt11  13416  cnmpt21  13424  setsmsbasg  13612  bdbl  13636  dvmulxxbr  13799  dvimulf  13803  dvcj  13806  dvfre  13807  dvrecap  13810  dvef  13821  sinperlem  13862  coshalfpip  13876  ptolemy  13878  tangtx  13892  relogef  13918  rpcxpadd  13959  rpmulcxp  13963  rpdivcxp  13965  cxpmul  13966  abscxp  13968  rpcxpsqrt  13975  rpabscxpbnd  13992  rplogbreexp  14004  rprelogbmul  14006  rprelogbdiv  14008  lgsneg  14058  lgsmod  14060  lgsdir2  14067  lgsdirprm  14068  lgsdir  14069  lgsdi  14071  lgssq  14074  lgssq2  14075  lgsdirnn0  14081  lgsdinn0  14082  2sqlem3  14086  bj-charfundcALT  14183  nninfsellemeqinf  14388  refeq  14399
  Copyright terms: Public domain W3C validator