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

Theorem 3eqtr3d 2080
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 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2074 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2074 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  mpteqb  5261  fvmptt  5262  fsnunfv  5363  f1ocnvfv1  5417  f1ocnvfv2  5418  fcof1  5423  caov12d  5682  caov13d  5684  caov411d  5686  caovimo  5694  grprinvlem  5695  grprinvd  5696  grpridd  5697  tfrlem5  5930  tfrlemiubacc  5944  nndir  6069  fopwdom  6310  addassnqg  6480  distrnqg  6485  enq0tr  6532  distrnq0  6557  distnq0r  6561  addnqprl  6627  addnqpru  6628  appdivnq  6661  ltmprr  6740  addcmpblnr  6824  mulcmpblnrlemg  6825  ltsrprg  6832  1idsr  6853  pn0sr  6856  mulgt0sr  6862  axmulass  6947  ax0id  6952  recriota  6964  mul12  7142  mul4  7145  readdcan  7153  add12  7169  cnegexlem2  7187  addcan  7191  ppncan  7253  addsub4  7254  muladd  7381  mulcanapd  7642  receuap  7650  div13ap  7672  divdivdivap  7689  divcanap5  7690  divdivap1  7699  divdivap2  7700  halfaddsub  8159  fztp  8940  fseq1p1m1  8956  flqzadd  9140  flqdiv  9163  iseqm1  9227  iseqcaopr  9242  exprecap  9296  expsubap  9302  zesq  9367  shftval3  9428  crre  9457  resub  9470  imsub  9478  cjsub  9492  climshft2  9827  qdencn  10124
  Copyright terms: Public domain W3C validator