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

Theorem 3eqtr3d 2122
 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 2116 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2116 1 (𝜑𝐶 = 𝐷)
 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:  mpteqb  5293  fvmptt  5294  fsnunfv  5395  f1ocnvfv1  5448  f1ocnvfv2  5449  fcof1  5454  caov12d  5713  caov13d  5715  caov411d  5717  caovimo  5725  grprinvlem  5726  grprinvd  5727  grpridd  5728  tfrlem5  5963  tfrlemiubacc  5979  tfr1onlemubacc  5995  tfrcllemubacc  6008  nndir  6134  fopwdom  6380  addassnqg  6634  distrnqg  6639  enq0tr  6686  distrnq0  6711  distnq0r  6715  addnqprl  6781  addnqpru  6782  appdivnq  6815  ltmprr  6894  addcmpblnr  6978  mulcmpblnrlemg  6979  ltsrprg  6986  1idsr  7007  pn0sr  7010  mulgt0sr  7016  axmulass  7101  ax0id  7106  recriota  7118  mul12  7304  mul4  7307  readdcan  7315  add12  7333  cnegexlem2  7351  addcan  7355  ppncan  7417  addsub4  7418  subaddeqd  7540  muladd  7555  mulcanapd  7818  receuap  7826  div13ap  7848  divdivdivap  7868  divcanap5  7869  divdivap1  7878  divdivap2  7879  halfaddsub  8332  fztp  9171  fseq1p1m1  9187  flqzadd  9380  flqdiv  9403  mulp1mod1  9447  modqnegd  9461  modqsub12d  9463  q2submod  9467  modsumfzodifsn  9478  iseqm1  9543  iseqcaopr  9558  exprecap  9614  expsubap  9621  zesq  9688  nn0opthlem1d  9744  facnn2  9758  faclbnd6  9768  shftval3  9853  crre  9882  resub  9895  imsub  9903  cjsub  9917  climshft2  10283  gcdaddm  10519  modgcd  10526  bezoutlemnewy  10529  absmulgcd  10550  gcdmultiplez  10554  eucialg  10585  lcmgcd  10604  lcmid  10606  qdencn  10943
 Copyright terms: Public domain W3C validator