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

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

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2
2 3eqtrd.2 . . 3  C
3 3eqtrd.3 . . 3  C  D
42, 3eqtrd 2069 . 2  D
51, 4eqtrd 2069 1  D
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  tpeq123d  3453  diftpsn3  3496  oteq123d  3555  resiima  4626  fvun1  5182  fvmptd  5196  fmptpr  5298  caovlem2d  5635  offval  5661  fnofval  5663  cnvf1olem  5787  nnm1  6033  ltexnqq  6391  prarloclemarch  6401  ltrnqg  6403  nq02m  6447  prarloclemcalc  6484  mulnqprl  6548  mulnqpru  6549  ltexprlemloc  6580  addcanprleml  6587  recexprlem1ssu  6605  cauappcvgprlem1  6630  axmulass  6737  axrnegex  6743  addcan2  6969  addsub  6999  subsub2  7015  negsubdi2  7046  muladd  7157  mulsub  7174  cru  7366  mulreim  7368  recextlem1  7394  mulap0  7397  muleqadd  7411  divrecap  7429  div23ap  7432  div12ap  7435  divcanap7  7459  conjmulap  7467  apmul1  7526  nndivtr  7716  qapne  8330  xnegneg  8496  fseq1p1m1  8706  nn0split  8744  fzosplitsnm1  8815  fzosplitprm1  8840  frecuzrdgsuc  8862  exp1  8895  expnegap0  8897  expmulzap  8935  expdivap  8939  binom3  8999  crim  9066  remullem  9079  remul2  9081  immul2  9088  ipcnval  9094  cjreim  9111  absid  9205
  Copyright terms: Public domain W3C validator