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

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

Proof of Theorem 3eqtrd
StepHypRef Expression
1 3eqtrd.1 . 2 (φA = B)
2 3eqtrd.2 . . 3 (φB = 𝐶)
3 3eqtrd.3 . . 3 (φ𝐶 = 𝐷)
42, 3eqtrd 2069 . 2 (φB = 𝐷)
51, 4eqtrd 2069 1 (φA = 𝐷)
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  6448  prarloclemcalc  6485  mulnqprl  6549  mulnqpru  6550  ltexprlemloc  6581  addcanprleml  6588  recexprlem1ssu  6606  cauappcvgprlem1  6631  axmulass  6757  axrnegex  6763  addcan2  6989  addsub  7019  subsub2  7035  negsubdi2  7066  muladd  7177  mulsub  7194  cru  7386  mulreim  7388  recextlem1  7414  mulap0  7417  muleqadd  7431  divrecap  7449  div23ap  7452  div12ap  7455  divcanap7  7479  conjmulap  7487  apmul1  7546  nndivtr  7736  qapne  8350  xnegneg  8516  fseq1p1m1  8726  nn0split  8764  fzosplitsnm1  8835  fzosplitprm1  8860  frecuzrdgsuc  8882  exp1  8915  expnegap0  8917  expmulzap  8955  expdivap  8959  binom3  9019  crim  9086  remullem  9099  remul2  9101  immul2  9108  ipcnval  9114  cjreim  9131  absid  9225
  Copyright terms: Public domain W3C validator