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

Theorem 3eqtr4d 2180
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  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4d
StepHypRef Expression
1 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
2 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
3 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
42, 3eqtr4d 2173 . 2  |-  ( ph  ->  D  =  A )
51, 4eqtr4d 2173 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  fnsnfv  5473  fvco2  5483  resfunexg  5634  fcof1  5677  fliftfun  5690  caovdir2d  5940  caov32d  5944  caov31d  5946  caov4d  5948  caovlem2d  5956  caofcom  5998  cnvf1olem  6114  tfrlem1  6198  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  frecrdg  6298  oav2  6352  omv2  6354  omsuc  6361  nnmsucr  6377  ecovicom  6530  ecoviass  6532  ecovidi  6534  carden2bex  7038  addcompig  7130  addasspig  7131  mulcompig  7132  mulasspig  7133  distrpig  7134  addassnqg  7183  addnq0mo  7248  mulnq0mo  7249  nqnq0a  7255  nqnq0m  7256  distrnq0  7260  mulcomnq0  7261  addassnq0  7263  addcmpblnr  7540  mulcmpblnrlemg  7541  addsrmo  7544  mulsrmo  7545  ltsrprg  7548  recexgt0sr  7574  mulgt0sr  7579  mulextsr1lem  7581  addcnsrec  7643  mulcnsrec  7644  pitonnlem2  7648  recidpirqlemcalc  7658  axaddcom  7671  adddir  7750  mul32  7885  mul31  7886  add32  7914  add4  7916  sub32  7989  sub4  8000  subdir  8141  mulneg2  8151  mulreim  8359  apadd1  8363  apneg  8366  divassap  8443  divdirap  8450  divmul13ap  8468  divmul24ap  8469  divdiv32ap  8473  conjmulap  8482  zeo  9149  xaddcom  9637  xnegdi  9644  xaddass  9645  xaddass2  9646  xpncan  9647  xadd4d  9661  lincmb01cmp  9779  iccf1o  9780  flhalf  10068  modqvalp1  10109  modqdi  10158  modqsubdir  10159  frecuzrdgg  10182  seq3shft2  10239  seq3caopr3  10247  seq3caopr  10249  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3homo  10276  seqfeq3  10278  seq3distr  10279  expp1  10293  expnegap0  10294  expaddzaplem  10329  expaddzap  10330  expmulzap  10332  sqneg  10345  sqdivap  10350  subsq2  10393  binom2  10396  facp1  10469  bcm1k  10499  bcp1n  10500  bcval5  10502  omgadd  10541  hashun  10544  hashxp  10565  shftfibg  10585  shftfib  10588  shftval  10590  2shfti  10596  seq3shft  10603  crre  10622  remim  10625  mulreap  10629  reneg  10633  readd  10634  remullem  10636  redivap  10639  imneg  10641  imadd  10642  imdivap  10646  cjcj  10648  cjadd  10649  cjmulrcl  10652  cjneg  10655  imval2  10659  resqrexlemcalc1  10779  absneg  10815  sqabsadd  10820  sqabssub  10821  absmul  10834  absresq  10843  absexp  10844  absexpzap  10845  bdtrilem  11003  xrmaxiflemcom  11011  xrmaxadd  11023  xrminrecl  11035  xrminadd  11037  serf0  11114  summodclem3  11142  fsum3  11149  isumss  11153  fisumss  11154  fsumadd  11168  isummulc1  11189  isumdivapc  11190  fsum2dlemstep  11196  fisumcom2  11200  fisum0diag2  11209  fsummulc2  11210  fsummulc1  11211  fsumdivapc  11212  fsumconst  11216  telfsumo  11228  fsumparts  11232  binomlem  11245  isumshft  11252  arisum2  11261  geolim  11273  geo2sum  11276  geo2lim  11278  cvgratnnlemseq  11288  cvgratz  11294  mertenslem2  11298  prodfrecap  11308  prodfdivap  11309  efcllemp  11353  efcj  11368  efexp  11377  resinval  11411  recosval  11412  cosneg  11423  efival  11428  sinadd  11432  cosadd  11433  addcos  11442  sin2t  11445  cos2t  11446  odd2np1lem  11558  oexpneg  11563  neggcd  11660  gcdabs2  11667  mulgcd  11693  mulgcdr  11695  gcddiv  11696  rplpwr  11704  eucalgval  11724  eucalginv  11726  eucalg  11729  neglcm  11745  lcmgcd  11748  mulgcddvds  11764  qredeu  11767  nn0gcdsq  11867  phimullem  11890  ennnfonelemp1  11908  setsabsd  11987  setscom  11988  tgdom  12230  txbasval  12425  cnmpt11  12441  cnmpt21  12449  setsmsbasg  12637  bdbl  12661  dvmulxxbr  12824  dvimulf  12828  dvcj  12831  dvfre  12832  dvrecap  12835  dvef  12845  sinperlem  12878  coshalfpip  12892  ptolemy  12894  tangtx  12908  nninfalllemn  13191  nninfsellemeqinf  13201  refeq  13212
  Copyright terms: Public domain W3C validator