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

Theorem 3eqtr3d 2156
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
31, 2eqtr3d 2150 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2150 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  mpteqb  5477  fvmptt  5478  fsnunfv  5587  f1ocnvfv1  5644  f1ocnvfv2  5645  fcof1  5650  caov12d  5918  caov13d  5920  caov411d  5922  caovimo  5930  grprinvlem  5931  grprinvd  5932  grpridd  5933  tfrlem5  6177  tfrlemiubacc  6193  tfr1onlemubacc  6209  tfrcllemubacc  6222  nndir  6352  fopwdom  6696  updjud  6933  omp1eomlem  6945  addassnqg  7154  distrnqg  7159  enq0tr  7206  distrnq0  7231  distnq0r  7235  addnqprl  7301  addnqpru  7302  appdivnq  7335  ltmprr  7414  addcmpblnr  7511  mulcmpblnrlemg  7512  ltsrprg  7519  1idsr  7540  pn0sr  7543  mulgt0sr  7550  map2psrprg  7577  axmulass  7645  ax0id  7650  recriota  7662  mul12  7855  mul4  7858  readdcan  7866  add12  7884  cnegexlem2  7902  addcan  7906  ppncan  7968  addsub4  7969  subeqxfrd  8089  subaddeqd  8095  muladd  8110  mulcanapd  8385  receuap  8393  div13ap  8416  divdivdivap  8436  divcanap5  8437  divdivap1  8446  divdivap2  8447  halfaddsub  8908  fztp  9809  fseq1p1m1  9825  flqzadd  10022  flqdiv  10045  mulp1mod1  10089  modqnegd  10103  modqsub12d  10105  q2submod  10109  modsumfzodifsn  10120  seq3m1  10192  seq3caopr  10207  iseqf1olemab  10213  iseqf1olemnanb  10214  seq3f1olemqsumk  10223  exprecap  10285  expsubap  10292  zesq  10361  nn0opthlem1d  10417  facnn2  10431  faclbnd6  10441  zfz1isolemsplit  10532  seq3coll  10536  shftval3  10550  crre  10580  resub  10593  imsub  10601  cjsub  10615  bdtrilem  10961  bdtri  10962  climshft2  11026  isummolemnm  11099  fsumf1o  11110  isumss  11111  fisumss  11112  fsumadd  11126  isumclim3  11143  fsummulc2  11168  fsumsub  11172  telfsumo  11186  telfsumo2  11187  hashiun  11198  bcxmas  11209  isumshft  11210  trireciplem  11220  geoserap  11227  geo2sum2  11235  sinsub  11357  cossub  11358  gcdaddm  11579  modgcd  11586  bezoutlemnewy  11591  absmulgcd  11612  gcdmultiplez  11616  eucalg  11647  lcmgcd  11666  lcmid  11668  numdensq  11786  dfphi2  11802  phiprm  11805  hashgcdlem  11809  ennnfonelem1  11826  ennnfonelemex  11833  topnpropgd  12040  restin  12251  blpnfctr  12514  xmssym  12544  limcimolemlt  12708  dvmulxxbr  12741  dvrecap  12752  dvmptaddx  12756  dvmptmulx  12757  dvmptnegcn  12759  dvmptsubcn  12760  dveflem  12761  peano4nninf  13034  nninfalllem1  13037  nninfall  13038  nninfsellemqall  13045  qdencn  13056
  Copyright terms: Public domain W3C validator