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

Theorem 3eqtrd 2118
Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)
Hypotheses
Ref Expression
3eqtrd.1  |-  ( ph  ->  A  =  B )
3eqtrd.2  |-  ( ph  ->  B  =  C )
3eqtrd.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtrd  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2  |-  ( ph  ->  A  =  B )
2 3eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
3 3eqtrd.3 . . 3  |-  ( ph  ->  C  =  D )
42, 3eqtrd 2114 . 2  |-  ( ph  ->  B  =  D )
51, 4eqtrd 2114 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  tpeq123d  3492  diftpsn3  3535  oteq123d  3593  resiima  4713  fvun1  5271  fvmptd  5285  fmptpr  5387  caovlem2d  5724  offval  5750  fnofval  5752  cnvf1olem  5876  nnm1  6163  ltexnqq  6660  prarloclemarch  6670  ltrnqg  6672  nq02m  6717  prarloclemcalc  6754  mulnqprl  6820  mulnqpru  6821  ltexprlemloc  6859  addcanprleml  6866  recexprlem1ssu  6886  cauappcvgprlem1  6911  caucvgsrlemfv  7029  caucvgsrlemoffval  7034  recidpirqlemcalc  7087  axmulass  7101  axrnegex  7107  muladd11r  7331  addcan2  7356  addsub  7386  subsub2  7403  negsubdi2  7434  muladd  7555  mulsub  7572  cru  7769  mulreim  7771  recextlem1  7808  mulap0  7811  muleqadd  7825  divrecap  7843  div23ap  7846  div12ap  7849  divmulasscomap  7851  divcanap7  7876  conjmulap  7884  apmul1  7943  nndivtr  8147  xp1d2m1eqxm1d2  8350  div4p1lem1div2  8351  qapne  8805  xnegneg  8976  fseq1p1m1  9187  nn0split  9224  fzosplitsnm1  9295  fzosplitprm1  9320  ceilid  9397  flqdiv  9403  zmod10  9422  modqcyc  9441  modqaddabs  9444  mulqaddmodid  9446  modqadd2mod  9456  modqm1p1mod0  9457  modqmul12d  9460  modqadd12d  9462  modqmulmodr  9472  modqaddmulmod  9473  frecuzrdgsuc  9496  iseqid3s  9562  iseqid  9563  iseqhomo  9565  iseqz  9566  exp1  9579  expnegap0  9581  expmulzap  9619  m1expeven  9620  expdivap  9624  binom3  9687  sqoddm1div8  9722  bcn1  9782  bcnp1n  9783  ibcval5  9787  bcn2m1  9793  bcn2p1  9794  crim  9883  remullem  9896  remul2  9898  immul2  9905  ipcnval  9911  cjreim  9928  recvguniqlem  10018  resqrexlemover  10034  resqrexlemcalc1  10038  absid  10095  amgm2  10142  max0addsup  10243  dvds2ln  10373  dvdseq  10393  opeo  10441  bezoutlemnewy  10529  eucalginv  10582  eucalglt  10583  eucialg  10585  lcmgcdlem  10603  lcm1  10607  divgcdcoprmex  10628  2sqpwodd  10698
  Copyright terms: Public domain W3C validator