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

Theorem 3eqtr3d 2158
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 2152 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2152 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  mpteqb  5479  fvmptt  5480  fsnunfv  5589  f1ocnvfv1  5646  f1ocnvfv2  5647  fcof1  5652  caov12d  5920  caov13d  5922  caov411d  5924  caovimo  5932  grprinvlem  5933  grprinvd  5934  grpridd  5935  tfrlem5  6179  tfrlemiubacc  6195  tfr1onlemubacc  6211  tfrcllemubacc  6224  nndir  6354  fopwdom  6698  updjud  6935  omp1eomlem  6947  addassnqg  7158  distrnqg  7163  enq0tr  7210  distrnq0  7235  distnq0r  7239  addnqprl  7305  addnqpru  7306  appdivnq  7339  ltmprr  7418  addcmpblnr  7515  mulcmpblnrlemg  7516  ltsrprg  7523  1idsr  7544  pn0sr  7547  mulgt0sr  7554  map2psrprg  7581  axmulass  7649  ax0id  7654  recriota  7666  mul12  7859  mul4  7862  readdcan  7870  add12  7888  cnegexlem2  7906  addcan  7910  ppncan  7972  addsub4  7973  subeqxfrd  8093  subaddeqd  8099  muladd  8114  mulcanapd  8389  receuap  8397  div13ap  8420  divdivdivap  8440  divcanap5  8441  divdivap1  8450  divdivap2  8451  halfaddsub  8912  fztp  9813  fseq1p1m1  9829  flqzadd  10026  flqdiv  10049  mulp1mod1  10093  modqnegd  10107  modqsub12d  10109  q2submod  10113  modsumfzodifsn  10124  seq3m1  10196  seq3caopr  10211  iseqf1olemab  10217  iseqf1olemnanb  10218  seq3f1olemqsumk  10227  exprecap  10289  expsubap  10296  zesq  10365  nn0opthlem1d  10421  facnn2  10435  faclbnd6  10445  zfz1isolemsplit  10536  seq3coll  10540  shftval3  10554  crre  10584  resub  10597  imsub  10605  cjsub  10619  bdtrilem  10965  bdtri  10966  climshft2  11030  isummolemnm  11103  fsumf1o  11114  isumss  11115  fisumss  11116  fsumadd  11130  isumclim3  11147  fsummulc2  11172  fsumsub  11176  telfsumo  11190  telfsumo2  11191  hashiun  11202  bcxmas  11213  isumshft  11214  trireciplem  11224  geoserap  11231  geo2sum2  11239  sinsub  11361  cossub  11362  gcdaddm  11584  modgcd  11591  bezoutlemnewy  11596  absmulgcd  11617  gcdmultiplez  11621  eucalg  11652  lcmgcd  11671  lcmid  11673  numdensq  11791  dfphi2  11807  phiprm  11810  hashgcdlem  11814  ennnfonelem1  11831  ennnfonelemex  11838  topnpropgd  12045  restin  12256  blpnfctr  12519  xmssym  12549  limcimolemlt  12713  dvmulxxbr  12746  dvrecap  12757  dvmptaddx  12761  dvmptmulx  12762  dvmptnegcn  12764  dvmptsubcn  12765  dveflem  12766  sin0pilem1  12773  ptolemy  12816  peano4nninf  13096  nninfalllem1  13099  nninfall  13100  nninfsellemqall  13107  qdencn  13118
  Copyright terms: Public domain W3C validator