ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr4d Unicode 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  |-  ( 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 2153 . 2  |-  ( ph  ->  D  =  A )
51, 4eqtr4d 2153 1  |-  ( ph  ->  C  =  D )
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  8333  apadd1  8337  apneg  8340  divassap  8417  divdirap  8424  divmul13ap  8442  divmul24ap  8443  divdiv32ap  8447  conjmulap  8456  zeo  9114  xaddcom  9599  xnegdi  9606  xaddass  9607  xaddass2  9608  xpncan  9609  xadd4d  9623  lincmb01cmp  9741  iccf1o  9742  flhalf  10030  modqvalp1  10071  modqdi  10120  modqsubdir  10121  frecuzrdgg  10144  seq3shft2  10201  seq3caopr3  10209  seq3caopr  10211  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3homo  10238  seqfeq3  10240  seq3distr  10241  expp1  10255  expnegap0  10256  expaddzaplem  10291  expaddzap  10292  expmulzap  10294  sqneg  10307  sqdivap  10312  subsq2  10355  binom2  10358  facp1  10431  bcm1k  10461  bcp1n  10462  bcval5  10464  omgadd  10503  hashun  10506  hashxp  10527  shftfibg  10547  shftfib  10550  shftval  10552  2shfti  10558  seq3shft  10565  crre  10584  remim  10587  mulreap  10591  reneg  10595  readd  10596  remullem  10598  redivap  10601  imneg  10603  imadd  10604  imdivap  10608  cjcj  10610  cjadd  10611  cjmulrcl  10614  cjneg  10617  imval2  10621  resqrexlemcalc1  10741  absneg  10777  sqabsadd  10782  sqabssub  10783  absmul  10796  absresq  10805  absexp  10806  absexpzap  10807  bdtrilem  10965  xrmaxiflemcom  10973  xrmaxadd  10985  xrminrecl  10997  xrminadd  10999  serf0  11076  summodclem3  11104  fsum3  11111  isumss  11115  fisumss  11116  fsumadd  11130  isummulc1  11151  isumdivapc  11152  fsum2dlemstep  11158  fisumcom2  11162  fisum0diag2  11171  fsummulc2  11172  fsummulc1  11173  fsumdivapc  11174  fsumconst  11178  telfsumo  11190  fsumparts  11194  binomlem  11207  isumshft  11214  arisum2  11223  geolim  11235  geo2sum  11238  geo2lim  11240  cvgratnnlemseq  11250  cvgratz  11256  mertenslem2  11260  efcllemp  11278  efcj  11293  efexp  11302  resinval  11336  recosval  11337  cosneg  11348  efival  11353  sinadd  11357  cosadd  11358  addcos  11367  sin2t  11370  cos2t  11371  odd2np1lem  11481  oexpneg  11486  neggcd  11583  gcdabs2  11590  mulgcd  11616  mulgcdr  11618  gcddiv  11619  rplpwr  11627  eucalgval  11647  eucalginv  11649  eucalg  11652  neglcm  11668  lcmgcd  11671  mulgcddvds  11687  qredeu  11690  nn0gcdsq  11789  phimullem  11812  ennnfonelemp1  11830  setsabsd  11909  setscom  11910  tgdom  12152  txbasval  12347  cnmpt11  12363  cnmpt21  12371  setsmsbasg  12559  bdbl  12583  dvmulxxbr  12746  dvimulf  12750  dvcj  12753  dvfre  12754  dvrecap  12757  dvef  12767  sinperlem  12800  coshalfpip  12814  ptolemy  12816  nninfalllemn  13098  nninfsellemeqinf  13108  refeq  13119
  Copyright terms: Public domain W3C validator