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

Theorem eqtrd 2072
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrd.1 (𝜑𝐴 = 𝐵)
eqtrd.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtrd (𝜑𝐴 = 𝐶)

Proof of Theorem eqtrd
StepHypRef Expression
1 eqtrd.1 . 2 (𝜑𝐴 = 𝐵)
2 eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
32eqeq2d 2051 . 2 (𝜑 → (𝐴 = 𝐵𝐴 = 𝐶))
41, 3mpbid 135 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:  eqtr2d  2073  eqtr3d  2074  eqtr4d  2075  3eqtrd  2076  3eqtrrd  2077  3eqtr2d  2078  syl5eq  2084  syl6eq  2088  rabeqbidv  2552  rabeqbidva  2553  csbidmg  2902  csbco3g  2904  difeq12d  3063  ifeq12d  3347  ifbieq1d  3350  ifbieq2d  3352  ifbieq12d  3354  csbsng  3431  disjpr2  3434  csbunig  3588  iuneq12d  3681  unisn3  4180  op1stbg  4210  opthreg  4280  onsucuni2  4288  csbxpg  4421  coeq12d  4500  csbdmg  4529  dmxpinm  4556  xpid11m  4557  reseq12d  4613  csbresg  4615  resima2  4644  imaeq12d  4669  csbrng  4782  opswapg  4807  relcnvtr  4840  relcoi2  4848  relcoi1  4849  iotaint  4880  funprg  4949  funtpg  4950  funcnvres2  4974  fnco  5007  fococnv2  5152  fveq12d  5184  csbfv12g  5209  csbfv2g  5210  csbfvg  5211  dffn5im  5219  funfvdm2  5237  fvun1  5239  fvmpt2d  5257  fvmptt  5262  fndmin  5274  fniniseg2  5289  fnniniseg2  5290  fmptcof  5331  fvresi  5356  fvunsng  5357  fvpr1g  5367  fvpr2g  5368  fvtp1g  5369  funiunfvdm  5402  fcof1o  5429  riotaeqbidv  5471  oveq123d  5533  csbov12g  5544  csbov1g  5545  csbov2g  5546  ovmpt2dxf  5626  caov42d  5687  caovdilemd  5692  caovimo  5694  grprinvd  5696  offval2  5726  caofinvl  5733  ot1stg  5779  ot2ndg  5780  2nd1st  5806  mpt2mptsx  5823  dmmpt2ssx  5825  fmpt2x  5826  fmpt2co  5837  1stconst  5842  algrflemg  5851  tfrexlem  5948  rdgivallem  5968  rdgisuc1  5971  frec0g  5983  frecsuclem1  5987  frecsuclem3  5990  frecrdg  5992  oa0  6037  oasuc  6044  oa1suc  6047  omsuc  6051  nnaass  6064  nndi  6065  nnmass  6066  nnm2  6098  nn2m  6099  ereq1  6113  errn  6128  uniqs2  6166  oviec  6212  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  phplem4on  6329  fidifsnen  6331  mulidpi  6414  addasspig  6426  mulasspig  6428  distrpig  6429  indpi  6438  addcmpblnq  6463  mulpipq  6468  dmaddpqlem  6473  nqpi  6474  addcomnqg  6477  recrecnq  6490  ltsonq  6494  ltanqg  6496  ltmnqg  6497  ltaddnq  6503  ltexnqq  6504  archnqq  6513  prarloclemarch  6514  ltrnqg  6516  ltnnnq  6519  nq0nn  6538  addcmpblnq0  6539  nqpnq0nq  6549  nqnq0a  6550  nq0m0r  6552  nq0a0  6553  distrnq0  6555  addassnq0  6558  nq02m  6561  prarloclemlo  6590  prarloclemcalc  6598  addnqprllem  6623  addnqprulem  6624  addnqprl  6625  addnqpru  6626  appdivnq  6659  mulnqprl  6664  mulnqpru  6665  addcanprlemu  6711  ltaprlem  6714  ltmprr  6738  cauappcvgprlemladdrl  6753  mulcmpblnrlemg  6823  mulcomsrg  6840  distrsrg  6842  ltsosr  6847  1idsr  6851  00sr  6852  ltasrg  6853  recexgt0sr  6856  srpospr  6865  prsradd  6868  prsrriota  6870  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsrlemoffres  6882  caucvgsr  6884  elreal2  6905  mulresr  6912  pitonnlem1p1  6920  pitonnlem2  6921  pitoregt0  6923  recidpirqlemcalc  6931  recidpirq  6932  axaddcl  6938  axmulcl  6940  axmulcom  6943  axmulass  6945  axdistr  6946  ax1rid  6949  axcnre  6953  recriota  6962  axcaucvglemcau  6970  mulid1  7022  mulid2  7023  joinlmuladdmuld  7051  muladd11  7144  1p1times  7145  readdcan  7151  add42  7171  npcan  7218  addsubass  7219  2addsub  7223  addsubeq4  7224  nppcan  7231  nnpcan  7232  npncan2  7236  nncan  7238  subsub  7239  nnncan  7244  nnncan1  7245  pnpcan2  7249  pnncan  7250  subneg  7258  negneg  7259  negdi2  7267  mul02  7382  mul01  7384  mulneg1  7390  mul2neg  7393  mulm1  7395  ltadd2  7414  rimul  7574  rereim  7575  mulreim  7593  recextlem1  7630  mulcanapd  7640  divcanap1  7658  divrecap2  7666  divcanap4  7674  dividap  7676  divdivdivap  7687  recdivap  7692  divadddivap  7701  divsubdivap  7702  div2negap  7709  divcanap5rd  7790  dmdcanap2d  7793  recgt0  7814  lt2mul2div  7843  nnmulcl  7933  times2  8037  add1p1  8172  sub1m1  8173  cnm2m1cnm3  8174  nn0supp  8232  peano2z  8279  nneoor  8338  cnref1o  8580  rexneg  8741  iooidg  8776  iooval2  8782  icoshftf1o  8857  lincmb01cmp  8869  iccf1o  8870  fzval2  8875  fzsuc  8929  fzpred  8930  fztpval  8943  fseq1p1m1  8954  fzshftral  8968  fzo0to3tp  9073  fzo0sn0fzo1  9075  fzosplitsn  9087  fzosplitprm1  9088  fzisfzounsn  9090  rebtwn2zlemstep  9105  2tnp1ge0ge0  9141  frec2uzsucd  9161  frecuzrdgrrn  9168  frec2uzrdg  9169  frecuzrdglem  9171  frecuzrdgsuc  9175  frecfzennn  9177  iseqeq1  9188  iseqp1  9199  iseqfeq2  9203  iseqfveq  9204  iseqshft2  9206  iseq1p  9213  iseqid3s  9220  expivallem  9230  expinnval  9232  expp1  9236  expn1ap0  9239  mulexp  9268  expaddzaplem  9272  expaddzap  9273  expmul  9274  expp1zap  9277  expm1ap  9278  sqval  9286  subsq2  9333  binom2  9336  binom21  9337  binom3  9340  zesq  9341  bernneq  9343  shftdm  9397  shftval2  9401  shftval4  9403  shftval5  9404  shftcan1  9409  imre  9425  crre  9431  remim  9434  reim0b  9436  recj  9441  reneg  9442  readd  9443  resub  9444  remullem  9445  imcj  9449  imneg  9450  imadd  9451  imsub  9452  cjcj  9457  cjadd  9458  ipcnval  9460  cjneg  9464  cjsub  9466  cjexp  9467  imval2  9468  cjap  9480  resqrexlemf1  9580  resqrexlemfp1  9581  resqrexlemover  9582  resqrexlemcalc1  9586  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemcvg  9591  resqrtcl  9601  sqrtsq  9616  absneg  9622  absvalsq  9625  absvalsq2  9626  sqabsadd  9627  sqabssub  9628  absval2  9629  absreimsq  9639  absmul  9641  absexp  9649  absexpzap  9650  abssuble0  9673  abstri  9674  recan  9679  amgm2  9688  climshft2  9801  subcn2  9806  climaddc2  9824  clim2iser2  9832  climcvg1nlem  9842  sqr2irrlem  9851  ialgr0  9857  ialginv  9860  ialgcvg  9861  ialgfx  9865
  Copyright terms: Public domain W3C validator