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  6416  addasspig  6428  mulasspig  6430  distrpig  6431  indpi  6440  addcmpblnq  6465  mulpipq  6470  dmaddpqlem  6475  nqpi  6476  addcomnqg  6479  recrecnq  6492  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltaddnq  6505  ltexnqq  6506  archnqq  6515  prarloclemarch  6516  ltrnqg  6518  ltnnnq  6521  nq0nn  6540  addcmpblnq0  6541  nqpnq0nq  6551  nqnq0a  6552  nq0m0r  6554  nq0a0  6555  distrnq0  6557  addassnq0  6560  nq02m  6563  prarloclemlo  6592  prarloclemcalc  6600  addnqprllem  6625  addnqprulem  6626  addnqprl  6627  addnqpru  6628  appdivnq  6661  mulnqprl  6666  mulnqpru  6667  addcanprlemu  6713  ltaprlem  6716  ltmprr  6740  cauappcvgprlemladdrl  6755  mulcmpblnrlemg  6825  mulcomsrg  6842  distrsrg  6844  ltsosr  6849  1idsr  6853  00sr  6854  ltasrg  6855  recexgt0sr  6858  srpospr  6867  prsradd  6870  prsrriota  6872  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemoffres  6884  caucvgsr  6886  elreal2  6907  mulresr  6914  pitonnlem1p1  6922  pitonnlem2  6923  pitoregt0  6925  recidpirqlemcalc  6933  recidpirq  6934  axaddcl  6940  axmulcl  6942  axmulcom  6945  axmulass  6947  axdistr  6948  ax1rid  6951  axcnre  6955  recriota  6964  axcaucvglemcau  6972  mulid1  7024  mulid2  7025  joinlmuladdmuld  7053  muladd11  7146  1p1times  7147  readdcan  7153  add42  7173  npcan  7220  addsubass  7221  2addsub  7225  addsubeq4  7226  nppcan  7233  nnpcan  7234  npncan2  7238  nncan  7240  subsub  7241  nnncan  7246  nnncan1  7247  pnpcan2  7251  pnncan  7252  subneg  7260  negneg  7261  negdi2  7269  mul02  7384  mul01  7386  mulneg1  7392  mul2neg  7395  mulm1  7397  ltadd2  7416  rimul  7576  rereim  7577  mulreim  7595  recextlem1  7632  mulcanapd  7642  divcanap1  7660  divrecap2  7668  divcanap4  7676  dividap  7678  divdivdivap  7689  recdivap  7694  divadddivap  7703  divsubdivap  7704  div2negap  7711  divcanap5rd  7792  dmdcanap2d  7795  recgt0  7816  lt2mul2div  7845  nnmulcl  7935  times2  8039  add1p1  8174  sub1m1  8175  cnm2m1cnm3  8176  nn0supp  8234  peano2z  8281  nneoor  8340  cnref1o  8582  rexneg  8743  iooidg  8778  iooval2  8784  icoshftf1o  8859  lincmb01cmp  8871  iccf1o  8872  fzval2  8877  fzsuc  8931  fzpred  8932  fztpval  8945  fseq1p1m1  8956  fzshftral  8970  fzo0to3tp  9075  fzo0sn0fzo1  9077  fzosplitsn  9089  fzosplitprm1  9090  fzisfzounsn  9092  rebtwn2zlemstep  9107  2tnp1ge0ge0  9143  flqdiv  9163  modqvalr  9167  modqdiffl  9177  modqfrac  9179  modqmulnn  9184  frec2uzsucd  9187  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdglem  9197  frecuzrdgsuc  9201  frecfzennn  9203  iseqeq1  9214  iseqp1  9225  iseqfeq2  9229  iseqfveq  9230  iseqshft2  9232  iseq1p  9239  iseqid3s  9246  expivallem  9256  expinnval  9258  expp1  9262  expn1ap0  9265  mulexp  9294  expaddzaplem  9298  expaddzap  9299  expmul  9300  expp1zap  9303  expm1ap  9304  sqval  9312  subsq2  9359  binom2  9362  binom21  9363  binom3  9366  zesq  9367  bernneq  9369  shftdm  9423  shftval2  9427  shftval4  9429  shftval5  9430  shftcan1  9435  imre  9451  crre  9457  remim  9460  reim0b  9462  recj  9467  reneg  9468  readd  9469  resub  9470  remullem  9471  imcj  9475  imneg  9476  imadd  9477  imsub  9478  cjcj  9483  cjadd  9484  ipcnval  9486  cjneg  9490  cjsub  9492  cjexp  9493  imval2  9494  cjap  9506  resqrexlemf1  9606  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrtcl  9627  sqrtsq  9642  absneg  9648  absvalsq  9651  absvalsq2  9652  sqabsadd  9653  sqabssub  9654  absval2  9655  absreimsq  9665  absmul  9667  absexp  9675  absexpzap  9676  abssuble0  9699  abstri  9700  recan  9705  amgm2  9714  climshft2  9827  subcn2  9832  climaddc2  9850  clim2iser2  9858  climcvg1nlem  9868  sqr2irrlem  9877  ialgr0  9883  ialginv  9886  ialgcvg  9887  ialgfx  9891  qdencn  10124
  Copyright terms: Public domain W3C validator