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  2549  rabeqbidva  2550  csbidmg  2899  csbco3g  2901  difeq12d  3060  ifeq12d  3344  ifbieq1d  3347  ifbieq2d  3349  ifbieq12d  3351  csbsng  3428  disjpr2  3431  csbunig  3585  iuneq12d  3678  unisn3  4167  op1stbg  4197  opthreg  4265  onsucuni2  4273  csbxpg  4399  coeq12d  4478  csbdmg  4507  dmxpinm  4534  xpid11m  4535  reseq12d  4591  csbresg  4593  resima2  4622  imaeq12d  4647  csbrng  4760  opswapg  4785  relcnvtr  4818  relcoi2  4826  relcoi1  4827  iotaint  4858  funprg  4927  funtpg  4928  funcnvres2  4952  fnco  4985  fococnv2  5130  fveq12d  5162  csbfv12g  5187  csbfv2g  5188  csbfvg  5189  dffn5im  5197  funfvdm2  5215  fvun1  5217  fvmpt2d  5235  fvmptt  5240  fndmin  5252  fniniseg2  5267  fnniniseg2  5268  fmptcof  5309  fvresi  5334  fvunsng  5335  fvpr1g  5345  fvpr2g  5346  fvtp1g  5347  funiunfvdm  5380  fcof1o  5407  riotaeqbidv  5449  oveq123d  5511  csbov12g  5522  csbov1g  5523  csbov2g  5524  ovmpt2dxf  5604  caov42d  5665  caovdilemd  5670  caovimo  5672  grprinvd  5674  offval2  5704  caofinvl  5711  ot1stg  5757  ot2ndg  5758  2nd1st  5784  mpt2mptsx  5801  dmmpt2ssx  5803  fmpt2x  5804  fmpt2co  5815  1stconst  5820  algrflemg  5829  tfrexlem  5926  rdgivallem  5946  rdgisuc1  5949  frec0g  5961  frecsuclem1  5965  frecsuclem3  5968  frecrdg  5970  oa0  6015  oasuc  6022  oa1suc  6025  omsuc  6029  nnaass  6042  nndi  6043  nnmass  6044  nnm2  6076  nn2m  6077  ereq1  6091  errn  6106  uniqs2  6144  oviec  6190  ecovass  6193  ecoviass  6194  ecovdi  6195  ecovidi  6196  phplem4on  6307  fidifsnen  6309  mulidpi  6388  addasspig  6400  mulasspig  6402  distrpig  6403  indpi  6412  addcmpblnq  6437  mulpipq  6442  dmaddpqlem  6447  nqpi  6448  addcomnqg  6451  recrecnq  6464  ltsonq  6468  ltanqg  6470  ltmnqg  6471  ltaddnq  6477  ltexnqq  6478  archnqq  6487  prarloclemarch  6488  ltrnqg  6490  ltnnnq  6493  nq0nn  6512  addcmpblnq0  6513  nqpnq0nq  6523  nqnq0a  6524  nq0m0r  6526  nq0a0  6527  distrnq0  6529  addassnq0  6532  nq02m  6535  prarloclemlo  6564  prarloclemcalc  6572  addnqprllem  6597  addnqprulem  6598  addnqprl  6599  addnqpru  6600  appdivnq  6633  mulnqprl  6638  mulnqpru  6639  addcanprlemu  6685  ltaprlem  6688  ltmprr  6712  cauappcvgprlemladdrl  6727  mulcmpblnrlemg  6797  mulcomsrg  6814  distrsrg  6816  ltsosr  6821  1idsr  6825  00sr  6826  ltasrg  6827  recexgt0sr  6830  srpospr  6839  prsradd  6842  prsrriota  6844  caucvgsrlemcau  6849  caucvgsrlemgt1  6851  caucvgsrlemoffval  6852  caucvgsrlemoffres  6856  caucvgsr  6858  elreal2  6879  mulresr  6886  pitonnlem1p1  6894  pitonnlem2  6895  pitoregt0  6897  recidpirqlemcalc  6905  recidpirq  6906  axaddcl  6912  axmulcl  6914  axmulcom  6917  axmulass  6919  axdistr  6920  ax1rid  6923  axcnre  6927  recriota  6936  axcaucvglemcau  6944  mulid1  6996  mulid2  6997  muladd11  7117  1p1times  7118  readdcan  7124  add42  7144  npcan  7191  addsubass  7192  2addsub  7196  addsubeq4  7197  nppcan  7203  nnpcan  7204  npncan2  7208  nncan  7210  subsub  7211  nnncan  7216  nnncan1  7217  pnpcan2  7221  pnncan  7222  subneg  7230  negneg  7231  negdi2  7239  mul02  7354  mul01  7356  mulneg1  7362  mul2neg  7365  mulm1  7367  ltadd2  7386  rimul  7543  rereim  7544  mulreim  7562  recextlem1  7599  mulcanapd  7609  divcanap1  7627  divrecap2  7635  divcanap4  7643  dividap  7645  divdivdivap  7656  recdivap  7661  divadddivap  7670  divsubdivap  7671  div2negap  7678  divcanap5rd  7759  dmdcanap2d  7762  recgt0  7783  lt2mul2div  7812  nnmulcl  7902  times2  8004  add1p1  8138  sub1m1  8139  cnm2m1cnm3  8140  nn0supp  8197  peano2z  8244  nneoor  8303  cnref1o  8544  rexneg  8701  iooidg  8736  iooval2  8742  icoshftf1o  8817  lincmb01cmp  8829  iccf1o  8830  fzval2  8835  fzsuc  8889  fzpred  8890  fztpval  8903  fseq1p1m1  8914  fzshftral  8928  fzo0to3tp  9033  fzo0sn0fzo1  9035  fzosplitsn  9047  fzosplitprm1  9048  fzisfzounsn  9050  frec2uzsucd  9056  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdglem  9066  frecuzrdgsuc  9070  frecfzennn  9072  iseqeq1  9083  iseqp1  9094  iseqfeq2  9098  iseqfveq  9099  iseqshft2  9101  iseq1p  9108  iseqid3s  9115  expivallem  9125  expinnval  9127  expp1  9131  expn1ap0  9134  mulexp  9163  expaddzaplem  9167  expaddzap  9168  expmul  9169  expp1zap  9172  expm1ap  9173  sqval  9181  subsq2  9228  binom2  9231  binom21  9232  binom3  9235  zesq  9236  bernneq  9238  shftdm  9292  shftval2  9296  shftval4  9298  shftval5  9299  shftcan1  9304  imre  9320  crre  9326  remim  9329  reim0b  9331  recj  9336  reneg  9337  readd  9338  resub  9339  remullem  9340  imcj  9344  imneg  9345  imadd  9346  imsub  9347  cjcj  9352  cjadd  9353  ipcnval  9355  cjneg  9359  cjsub  9361  cjexp  9362  imval2  9363  cjap  9375  resqrexlemf1  9475  resqrexlemfp1  9476  resqrexlemover  9477  resqrexlemcalc1  9481  resqrexlemcalc3  9483  resqrexlemnm  9485  resqrexlemcvg  9486  resqrtcl  9496  sqrtsq  9511  absneg  9517  absvalsq  9520  absvalsq2  9521  sqabsadd  9522  sqabssub  9523  absval2  9524  absreimsq  9534  absmul  9536  absexp  9544  absexpzap  9545  abssuble0  9568  abstri  9569  recan  9574  amgm2  9583  climshft2  9695  subcn2  9700  climaddc2  9718  clim2iser2  9726  climcvg1nlem  9736  sqr2irrlem  9745  ialgr0  9751  ialginv  9754  ialgcvg  9755  ialgfx  9759
  Copyright terms: Public domain W3C validator