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  8390  receuap  8398  div13ap  8421  divdivdivap  8441  divcanap5  8442  divdivap1  8451  divdivap2  8452  halfaddsub  8922  fztp  9826  fseq1p1m1  9842  flqzadd  10039  flqdiv  10062  mulp1mod1  10106  modqnegd  10120  modqsub12d  10122  q2submod  10126  modsumfzodifsn  10137  seq3m1  10209  seq3caopr  10224  iseqf1olemab  10230  iseqf1olemnanb  10231  seq3f1olemqsumk  10240  exprecap  10302  expsubap  10309  zesq  10378  nn0opthlem1d  10434  facnn2  10448  faclbnd6  10458  zfz1isolemsplit  10549  seq3coll  10553  shftval3  10567  crre  10597  resub  10610  imsub  10618  cjsub  10632  bdtrilem  10978  bdtri  10979  climshft2  11043  isummolemnm  11116  fsumf1o  11127  isumss  11128  fisumss  11129  fsumadd  11143  isumclim3  11160  fsummulc2  11185  fsumsub  11189  telfsumo  11203  telfsumo2  11204  hashiun  11215  bcxmas  11226  isumshft  11227  trireciplem  11237  geoserap  11244  geo2sum2  11252  sinsub  11374  cossub  11375  gcdaddm  11599  modgcd  11606  bezoutlemnewy  11611  absmulgcd  11632  gcdmultiplez  11636  eucalg  11667  lcmgcd  11686  lcmid  11688  numdensq  11807  dfphi2  11823  phiprm  11826  hashgcdlem  11830  ennnfonelem1  11847  ennnfonelemex  11854  topnpropgd  12061  restin  12272  blpnfctr  12535  xmssym  12565  limcimolemlt  12729  dvmulxxbr  12762  dvrecap  12773  dvmptaddx  12777  dvmptmulx  12778  dvmptnegcn  12780  dvmptsubcn  12781  dveflem  12782  sin0pilem1  12789  ptolemy  12832  tangtx  12846  peano4nninf  13127  nninfalllem1  13130  nninfall  13131  nninfsellemqall  13138  qdencn  13149
  Copyright terms: Public domain W3C validator