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

Theorem 3eqtr3d 2218
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 2212 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2212 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  mpteqb  5602  fvmptt  5603  fsnunfv  5713  f1ocnvfv1  5772  f1ocnvfv2  5773  fcof1  5778  caov12d  6050  caov13d  6052  caov411d  6054  caovimo  6062  tfrlem5  6309  tfrlemiubacc  6325  tfr1onlemubacc  6341  tfrcllemubacc  6354  nndir  6485  fopwdom  6830  updjud  7075  omp1eomlem  7087  addassnqg  7369  distrnqg  7374  enq0tr  7421  distrnq0  7446  distnq0r  7450  addnqprl  7516  addnqpru  7517  appdivnq  7550  ltmprr  7629  addcmpblnr  7726  mulcmpblnrlemg  7727  ltsrprg  7734  1idsr  7755  pn0sr  7758  mulgt0sr  7765  map2psrprg  7792  axmulass  7860  ax0id  7865  recriota  7877  mul12  8073  mul4  8076  readdcan  8084  add12  8102  cnegexlem2  8120  addcan  8124  ppncan  8186  addsub4  8187  subeqxfrd  8307  subaddeqd  8313  muladd  8328  mulcanapd  8604  receuap  8612  div13ap  8636  divdivdivap  8656  divcanap5  8657  divdivap1  8666  divdivap2  8667  halfaddsub  9139  fztp  10061  fseq1p1m1  10077  flqzadd  10281  flqdiv  10304  mulp1mod1  10348  modqnegd  10362  modqsub12d  10364  q2submod  10368  modsumfzodifsn  10379  seq3m1  10451  seq3caopr  10466  iseqf1olemab  10472  iseqf1olemnanb  10473  seq3f1olemqsumk  10482  exprecap  10544  expsubap  10551  zesq  10621  nn0opthlem1d  10681  facnn2  10695  faclbnd6  10705  zfz1isolemsplit  10799  seq3coll  10803  shftval3  10817  crre  10847  resub  10860  imsub  10868  cjsub  10882  bdtrilem  11228  bdtri  11229  climshft2  11295  nnf1o  11365  fsumf1o  11379  isumss  11380  fisumss  11381  fsumadd  11395  isumclim3  11412  fsummulc2  11437  fsumsub  11441  telfsumo  11455  telfsumo2  11456  hashiun  11467  bcxmas  11478  isumshft  11479  trireciplem  11489  geoserap  11496  geo2sum2  11504  fprodf1o  11577  prodssdc  11578  fprodssdc  11579  fprodmul  11580  fprodm1  11587  sinsub  11729  cossub  11730  p1modz1  11782  gcdaddm  11965  modgcd  11972  bezoutlemnewy  11977  absmulgcd  11998  gcdmultiplez  12002  eucalg  12039  lcmgcd  12058  lcmid  12060  numdensq  12182  dfphi2  12200  phiprm  12203  fermltl  12214  prmdiveq  12216  hashgcdlem  12218  odzdvds  12225  powm2modprm  12232  modprm0  12234  coprimeprodsq  12237  pythagtriplem6  12250  pythagtriplem7  12251  pythagtriplem12  12255  pythagtriplem14  12257  pythagtriplem16  12259  pcaddlem  12318  sumhashdc  12325  fldivp1  12326  pcfac  12328  pockthlem  12334  ennnfonelem1  12388  ennnfonelemex  12395  topnpropgd  12647  grprinvlem  12693  grprinvd  12694  grpridd  12695  mnd12g  12718  grprcan  12797  grplcan  12818  grpasscan1  12819  grpinv11  12825  grpinvnz  12827  grplmulf1o  12830  grpinvpropdg  12831  grpinvadd  12834  grpsubsub4  12849  dfgrp3m  12855  mhmid  12865  mhmmnd  12866  mulgz  12896  mulgdirlem  12899  mulgdir  12900  mulgass  12905  mulgsubdir  12908  mulgpropdg  12910  ringcom  13037  crngpropd  13041  isringd  13043  ringlz  13045  ringrz  13046  ring1eq0  13048  ringmneg1  13053  mulgass3  13076  unitgrp  13107  rngidpropdg  13135  invrpropdg  13138  restin  13336  blpnfctr  13599  xmssym  13629  limcimolemlt  13793  dvmulxxbr  13826  dvrecap  13837  dvmptaddx  13841  dvmptmulx  13842  dvmptnegcn  13844  dvmptsubcn  13845  dvmptcjx  13846  dveflem  13847  sin0pilem1  13862  ptolemy  13905  tangtx  13919  rpcxpneg  13988  rpcxpsub  13989  cxprec  13991  rpcxproot  13994  cxpcom  14017  rpabscxpbnd  14019  lgsvalmod  14080  lgsneg  14085  lgsdilem  14088  lgsne0  14099  lgssq  14101  lgssq2  14102  peano4nninf  14404  nninfalllem1  14406  nninfall  14407  nninfsellemqall  14413  qdencn  14424
  Copyright terms: Public domain W3C validator