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

Theorem eqtrd 2088
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 2067 . 2 (𝜑 → (𝐴 = 𝐵𝐴 = 𝐶))
41, 3mpbid 139 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqtr2d  2089  eqtr3d  2090  eqtr4d  2091  3eqtrd  2092  3eqtrrd  2093  3eqtr2d  2094  syl5eq  2100  syl6eq  2104  rabeqbidv  2569  rabeqbidva  2570  csbidmg  2930  csbco3g  2932  difeq12d  3091  ifeq12d  3375  ifbieq1d  3378  ifbieq2d  3380  ifbieq12d  3382  csbsng  3459  disjpr2  3462  csbunig  3616  iuneq12d  3709  unisn3  4208  op1stbg  4238  opthreg  4308  onsucuni2  4316  csbxpg  4449  coeq12d  4528  csbdmg  4557  dmxpinm  4584  xpid11m  4585  reseq12d  4641  csbresg  4643  resima2  4672  imaeq12d  4697  csbrng  4810  opswapg  4835  relcnvtr  4868  relcoi2  4876  relcoi1  4877  iotaint  4908  funprg  4977  funtpg  4978  funcnvres2  5002  fnco  5035  fococnv2  5180  fveq12d  5212  csbfv12g  5237  csbfv2g  5238  csbfvg  5239  dffn5im  5247  funfvdm2  5265  fvun1  5267  fvmpt2d  5285  fvmptt  5290  fndmin  5302  fniniseg2  5317  fnniniseg2  5318  fmptcof  5359  fvresi  5384  fvunsng  5385  fvpr1g  5395  fvpr2g  5396  fvtp1g  5397  funiunfvdm  5430  fcof1o  5457  riotaeqbidv  5499  oveq123d  5561  csbov12g  5572  csbov1g  5573  csbov2g  5574  ovmpt2dxf  5654  caov42d  5715  caovdilemd  5720  caovimo  5722  grprinvd  5724  offval2  5754  caofinvl  5761  ot1stg  5807  ot2ndg  5808  2nd1st  5834  mpt2mptsx  5851  dmmpt2ssx  5853  fmpt2x  5854  fmpt2co  5865  1stconst  5870  algrflemg  5879  tfrexlem  5979  rdgivallem  5999  rdgisuc1  6002  frec0g  6014  frecsuclem1  6018  frecsuclem3  6021  frecrdg  6023  oa0  6068  oasuc  6075  oa1suc  6078  omsuc  6082  nnaass  6095  nndi  6096  nnmass  6097  nnm2  6129  nn2m  6130  ereq1  6144  errn  6159  uniqs2  6197  oviec  6243  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  phplem4on  6360  fidifsnen  6362  supeq2  6395  eqsupti  6402  mulidpi  6474  addasspig  6486  mulasspig  6488  distrpig  6489  indpi  6498  addcmpblnq  6523  mulpipq  6528  dmaddpqlem  6533  nqpi  6534  addcomnqg  6537  recrecnq  6550  ltsonq  6554  ltanqg  6556  ltmnqg  6557  ltaddnq  6563  ltexnqq  6564  archnqq  6573  prarloclemarch  6574  ltrnqg  6576  ltnnnq  6579  nq0nn  6598  addcmpblnq0  6599  nqpnq0nq  6609  nqnq0a  6610  nq0m0r  6612  nq0a0  6613  distrnq0  6615  addassnq0  6618  nq02m  6621  prarloclemlo  6650  prarloclemcalc  6658  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  appdivnq  6719  mulnqprl  6724  mulnqpru  6725  addcanprlemu  6771  ltaprlem  6774  ltmprr  6798  cauappcvgprlemladdrl  6813  mulcmpblnrlemg  6883  mulcomsrg  6900  distrsrg  6902  ltsosr  6907  1idsr  6911  00sr  6912  ltasrg  6913  recexgt0sr  6916  srpospr  6925  prsradd  6928  prsrriota  6930  caucvgsrlemcau  6935  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsrlemoffres  6942  caucvgsr  6944  elreal2  6965  mulresr  6972  pitonnlem1p1  6980  pitonnlem2  6981  pitoregt0  6983  recidpirqlemcalc  6991  recidpirq  6992  axaddcl  6998  axmulcl  7000  axmulcom  7003  axmulass  7005  axdistr  7006  ax1rid  7009  axcnre  7013  recriota  7022  axcaucvglemcau  7030  mulid1  7082  mulid2  7083  adddirp1d  7111  joinlmuladdmuld  7112  muladd11  7207  1p1times  7208  readdcan  7214  comraddd  7231  add42  7236  npcan  7283  addsubass  7284  2addsub  7288  addsubeq4  7289  nppcan  7296  nnpcan  7297  npncan2  7301  nncan  7303  subsub  7304  nnncan  7309  nnncan1  7310  pnpcan2  7314  pnncan  7315  subneg  7323  negneg  7324  negdi2  7332  mvrraddd  7438  subaddeqd  7439  addid0  7443  mul02  7456  mul01  7458  mulneg1  7464  mul2neg  7467  mulm1  7469  ltadd2  7488  rimul  7650  rereim  7651  mulreim  7669  recextlem1  7706  mulcanapd  7716  divcanap1  7734  divrecap2  7742  divcanap4  7750  dividap  7752  muldivdirap  7758  divdivdivap  7764  recdivap  7769  divadddivap  7778  divsubdivap  7779  div2negap  7786  divcanap5rd  7867  dmdcanap2d  7870  recgt0  7891  lt2mul2div  7920  nnmulcl  8011  times2  8112  add1p1  8231  sub1m1  8232  cnm2m1cnm3  8233  nn0supp  8291  peano2z  8338  nneoor  8399  cnref1o  8680  rexneg  8844  iooidg  8879  iooval2  8885  icoshftf1o  8960  lincmb01cmp  8972  iccf1o  8973  fzval2  8979  fzsuc  9033  fzpred  9034  fztpval  9047  fseq1p1m1  9058  fzshftral  9072  fzo0to3tp  9177  fzo0sn0fzo1  9179  fzosplitsn  9191  fzosplitprm1  9192  fzisfzounsn  9194  rebtwn2zlemstep  9209  2tnp1ge0ge0  9251  flqdiv  9271  modqvalr  9275  modqdiffl  9285  modqfrac  9287  modqmulnn  9292  modqid  9299  modqcyc  9309  modqcyc2  9310  mulp1mod1  9315  modqmuladd  9316  modqmuladdnn0  9318  qnegmod  9319  m1modnnsub1  9320  addmodid  9322  addmodidr  9323  modqmul12d  9328  modqnegd  9329  modqadd12d  9330  modifeq2int  9336  modqaddmulmod  9341  modqdi  9342  modqsubdir  9343  modsumfzodifsn  9346  addmodlteq  9348  frec2uzsucd  9351  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdglem  9361  frecuzrdgsuc  9365  frecfzennn  9367  iseqeq1  9378  iseqp1  9389  iseqfeq2  9393  iseqfveq  9394  iseqshft2  9396  iseq1p  9403  iseqid3s  9410  iseqz  9413  expivallem  9421  expinnval  9423  expp1  9427  expn1ap0  9430  mulexp  9459  expaddzaplem  9463  expaddzap  9464  expmul  9465  expp1zap  9469  expm1ap  9470  sqval  9478  iexpcyc  9523  subsq2  9526  binom2  9529  binom21  9530  mulbinom2  9533  binom3  9534  zesq  9535  bernneq  9537  sqoddm1div8  9569  nn0opthlem1d  9588  facp1  9598  faclbnd6  9612  bcval2  9618  bcval3  9619  bcn0  9623  bcp1n  9629  bcp1nk  9630  bcn2  9632  bcp1m1  9633  bcpasc  9634  bcn2m1  9637  shftdm  9651  shftval2  9655  shftval4  9657  shftval5  9658  shftcan1  9663  imre  9679  crre  9685  remim  9688  reim0b  9690  recj  9695  reneg  9696  readd  9697  resub  9698  remullem  9699  imcj  9703  imneg  9704  imadd  9705  imsub  9706  cjcj  9711  cjadd  9712  ipcnval  9714  cjneg  9718  cjsub  9720  cjexp  9721  imval2  9722  cjap  9734  resqrexlemf1  9835  resqrexlemfp1  9836  resqrexlemover  9837  resqrexlemcalc1  9841  resqrexlemcalc3  9843  resqrexlemnm  9845  resqrexlemcvg  9846  resqrtcl  9856  sqrtsq  9871  absneg  9877  absvalsq  9880  absvalsq2  9881  sqabsadd  9882  sqabssub  9883  absval2  9884  absreimsq  9894  absmul  9896  absexp  9906  absexpzap  9907  abssuble0  9930  abstri  9931  recan  9936  amgm2  9945  climshft2  10058  subcn2  10063  climaddc2  10081  clim2iser2  10089  climcvg1nlem  10099  dvdstr  10144  dvdsadd2b  10154  mulmoddvds  10175  ltoddhalfle  10205  opoe  10207  m1expo  10212  m1exp1  10213  flodddiv4  10246  flodddiv4t2lthalf  10249  sqr2irrlem  10250  ialgr0  10266  ialginv  10269  ialgcvg  10270  ialgfx  10274  qdencn  10511
  Copyright terms: Public domain W3C validator