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

Theorem eqtrd 2117
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtrd.1  |-  ( ph  ->  A  =  B )
eqtrd.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtrd  |-  ( ph  ->  A  =  C )

Proof of Theorem eqtrd
StepHypRef Expression
1 eqtrd.1 . 2  |-  ( ph  ->  A  =  B )
2 eqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32eqeq2d 2096 . 2  |-  ( ph  ->  ( A  =  B  <-> 
A  =  C ) )
41, 3mpbid 145 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqtr2d  2118  eqtr3d  2119  eqtr4d  2120  3eqtrd  2121  3eqtrrd  2122  3eqtr2d  2123  syl5eq  2129  syl6eq  2133  rabeqbidv  2610  rabeqbidva  2611  csbidmg  2973  csbco3g  2975  difeq12d  3108  ifeq12d  3396  ifbieq1d  3399  ifbieq2d  3401  ifbieq12d  3403  eqifdc  3411  csbsng  3486  disjpr2  3489  csbunig  3644  iuneq12d  3737  unisn3  4243  op1stbg  4273  opthreg  4344  onsucuni2  4352  csbxpg  4486  coeq12d  4567  csbdmg  4597  dmxpinm  4624  xpid11m  4625  reseq12d  4681  csbresg  4683  resima2  4712  imaeq12d  4739  csbrng  4855  opswapg  4880  relcnvtr  4913  relcoi2  4924  relcoi1  4925  iotaint  4956  funprg  5026  funtpg  5027  funcnvres2  5051  fnco  5084  fococnv2  5236  fveq12d  5269  csbfv12g  5297  csbfv2g  5298  csbfvg  5299  dffn5im  5307  funfvdm2  5325  fvun1  5327  fvmpt2d  5346  fvmptt  5351  fndmin  5363  fniniseg2  5378  fnniniseg2  5379  fmptcof  5422  fvresi  5447  fvunsng  5448  fvpr1g  5458  fvpr2g  5459  fvtp1g  5460  funiunfvdm  5497  fcof1o  5523  riotaeqbidv  5566  oveq123d  5628  csbov12g  5639  csbov1g  5640  csbov2g  5641  ovmpt2dxf  5721  caov42d  5782  caovdilemd  5787  caovimo  5789  grprinvd  5791  offval2  5821  caofinvl  5828  ot1stg  5874  ot2ndg  5875  2nd1st  5901  mpt2mptsx  5918  dmmpt2ssx  5920  fmpt2x  5921  fmpt2co  5932  1stconst  5937  algrflemg  5946  tfrexlem  6047  rdgivallem  6094  rdgisuc1  6097  frec0g  6110  frecabcl  6112  frecsuclem  6119  frecrdg  6121  oa0  6166  oasuc  6173  oa1suc  6176  omsuc  6181  nnaass  6194  nndi  6195  nnmass  6196  nnm2  6230  nn2m  6231  ereq1  6245  errn  6260  uniqs2  6298  oviec  6344  ecovass  6347  ecoviass  6348  ecovdi  6349  ecovidi  6350  mapsnconst  6397  mapen  6508  mapxpen  6510  xpmapenlem  6511  phplem4on  6529  fidifsnen  6532  undifdc  6580  fisseneq  6586  snexxph  6602  sbthlemi4  6606  sbthlemi6  6608  supeq2  6621  eqsupti  6628  infvalti  6654  djuf1olem  6682  djuss  6698  1stinl  6702  2ndinl  6703  1stinr  6704  2ndinr  6705  updjudhcoinlf  6708  updjudhcoinrg  6709  en2other2  6759  mulidpi  6814  addasspig  6826  mulasspig  6828  distrpig  6829  indpi  6838  addcmpblnq  6863  mulpipq  6868  dmaddpqlem  6873  nqpi  6874  addcomnqg  6877  recrecnq  6890  ltsonq  6894  ltanqg  6896  ltmnqg  6897  ltaddnq  6903  ltexnqq  6904  archnqq  6913  prarloclemarch  6914  ltrnqg  6916  ltnnnq  6919  nq0nn  6938  addcmpblnq0  6939  nqpnq0nq  6949  nqnq0a  6950  nq0m0r  6952  nq0a0  6953  distrnq0  6955  addassnq0  6958  nq02m  6961  prarloclemlo  6990  prarloclemcalc  6998  addnqprllem  7023  addnqprulem  7024  addnqprl  7025  addnqpru  7026  appdivnq  7059  mulnqprl  7064  mulnqpru  7065  addcanprlemu  7111  ltaprlem  7114  ltmprr  7138  cauappcvgprlemladdrl  7153  mulcmpblnrlemg  7223  mulcomsrg  7240  distrsrg  7242  ltsosr  7247  1idsr  7251  00sr  7252  ltasrg  7253  recexgt0sr  7256  srpospr  7265  prsradd  7268  prsrriota  7270  caucvgsrlemcau  7275  caucvgsrlemgt1  7277  caucvgsrlemoffval  7278  caucvgsrlemoffres  7282  caucvgsr  7284  elreal2  7305  mulresr  7312  pitonnlem1p1  7320  pitonnlem2  7321  pitoregt0  7323  recidpirqlemcalc  7331  recidpirq  7332  axaddcl  7338  axmulcl  7340  axmulcom  7343  axmulass  7345  axdistr  7346  ax1rid  7349  axcnre  7353  recriota  7362  axcaucvglemcau  7370  mulid1  7422  mulid2  7423  adddirp1d  7451  joinlmuladdmuld  7452  muladd11  7552  1p1times  7553  readdcan  7559  comraddd  7576  add42  7581  npcan  7628  addsubass  7629  2addsub  7633  addsubeq4  7634  nppcan  7641  nnpcan  7642  npncan2  7646  nncan  7648  subsub  7649  nnncan  7654  nnncan1  7655  pnpcan2  7659  pnncan  7660  subneg  7668  negneg  7669  negdi2  7677  mvrraddd  7783  subaddeqd  7784  addid0  7788  mul02  7802  mul01  7804  mulneg1  7810  mul2neg  7813  mulm1  7815  ltadd2  7834  rimul  7996  rereim  7997  mulreim  8015  recextlem1  8052  mulcanapd  8062  divcanap1  8080  divrecap2  8088  divmulassap  8094  divmulasscomap  8095  divcanap4  8098  dividap  8100  muldivdirap  8106  divdivdivap  8112  recdivap  8117  divadddivap  8126  divsubdivap  8127  div2negap  8134  divcanap5rd  8215  dmdcanap2d  8218  recgt0  8239  lt2mul2div  8268  nnmulcl  8371  times2  8472  add1p1  8591  sub1m1  8592  cnm2m1cnm3  8593  nn0supp  8651  peano2z  8712  nneoor  8774  supminfex  9010  cnref1o  9058  rexneg  9217  iooidg  9252  iooval2  9258  icoshftf1o  9333  lincmb01cmp  9345  iccf1o  9346  fzval2  9352  fzsuc  9406  fzpred  9407  fztpval  9420  fseq1p1m1  9431  fzshftral  9445  fzo0to3tp  9551  fzo0sn0fzo1  9553  fzosplitsn  9565  fzosplitprm1  9566  fzisfzounsn  9568  rebtwn2zlemstep  9585  2tnp1ge0ge0  9629  flqdiv  9649  modqvalr  9653  modqdiffl  9663  modqfrac  9665  modqmulnn  9670  modqid  9677  modqcyc  9687  modqcyc2  9688  mulp1mod1  9693  modqmuladd  9694  modqmuladdnn0  9696  qnegmod  9697  m1modnnsub1  9698  addmodid  9700  addmodidr  9701  modqmul12d  9706  modqnegd  9707  modqadd12d  9708  modifeq2int  9714  modqaddmulmod  9719  modqdi  9720  modqsubdir  9721  modsumfzodifsn  9724  addmodlteq  9726  frec2uzsucd  9729  frecuzrdgrrn  9736  frec2uzrdg  9737  frecuzrdglem  9739  frecuzrdgsuc  9742  frecuzrdgg  9744  frecuzrdgdomlem  9745  frecuzrdgfunlem  9747  frecuzrdgtclt  9749  frecuzrdgsuctlem  9751  frecfzennn  9754  iseqeq1  9775  iseqvalt  9783  iseqp1  9789  iseqp1t  9790  iseqoveq  9791  iseqfeq2  9796  iseqfveq  9797  iseqshft2  9799  iseq1p  9806  iseqf1olemnab  9814  iseqf1olemab  9815  iseqf1olemnanb  9816  iseqf1olemqk  9820  iseqf1olemfvp  9823  iseqf1olemqsumkj  9824  iseqf1olemqsumk  9825  iseqf1olemqsum  9826  iseqf1o  9830  iseqid3s  9834  iseqz  9838  fser0const  9842  expivallem  9847  expinnval  9849  expp1  9853  expn1ap0  9856  mulexp  9885  expaddzaplem  9889  expaddzap  9890  expmul  9891  expp1zap  9895  expm1ap  9896  sqval  9904  iexpcyc  9949  subsq2  9952  binom2  9955  binom21  9956  mulbinom2  9959  binom3  9960  zesq  9961  bernneq  9963  sqoddm1div8  9995  nn0opthlem1d  10017  facp1  10027  faclbnd6  10041  bcval2  10047  bcval3  10048  bcn0  10052  bcp1n  10058  bcp1nk  10059  bcn2  10061  bcp1m1  10062  bcpasc  10063  bcn2m1  10066  hashinfom  10075  hashennn  10077  hashfz1  10080  fseq1hash  10098  omgadd  10099  hashunsng  10104  hashprg  10105  hashdifsn  10116  hashdifpr  10117  hashfz  10118  hashfzo  10119  hashfzo0  10120  hashfzp1  10121  hashfz0  10122  hashxp  10123  resunimafz0  10125  fnfz0hash  10126  ffzo0hash  10128  hashfacen  10130  zfz1isolemsplit  10132  zfz1isolemiso  10133  zfz1isolem1  10134  shftdm  10145  shftval2  10149  shftval4  10151  shftval5  10152  shftcan1  10157  imre  10173  crre  10179  remim  10182  reim0b  10184  recj  10189  reneg  10190  readd  10191  resub  10192  remullem  10193  imcj  10197  imneg  10198  imadd  10199  imsub  10200  cjcj  10205  cjadd  10206  ipcnval  10208  cjneg  10212  cjsub  10214  cjexp  10215  imval2  10216  cjap  10228  resqrexlemf1  10329  resqrexlemfp1  10330  resqrexlemover  10331  resqrexlemcalc1  10335  resqrexlemcalc3  10337  resqrexlemnm  10339  resqrexlemcvg  10340  resqrtcl  10350  sqrtsq  10365  absneg  10371  absvalsq  10374  absvalsq2  10375  sqabsadd  10376  sqabssub  10377  absval2  10378  absreimsq  10388  absmul  10390  absexp  10400  absexpzap  10401  abssuble0  10424  abstri  10425  recan  10430  amgm2  10439  maxabslemlub  10528  max0addsup  10540  minmax  10547  climshft2  10580  subcn2  10585  climaddc2  10603  climcvg1nlem  10621  sumeq12dv  10644  sumeq12rdv  10645  isumrblem  10648  fisumcvg  10649  isummolem3  10652  isummolem2a  10653  isummo  10655  fisum  10658  isumz  10660  fsumf1o  10661  dvdstr  10700  dvdsadd2b  10710  mulmoddvds  10731  ltoddhalfle  10760  opoe  10762  m1expo  10767  m1exp1  10768  flodddiv4  10801  flodddiv4t2lthalf  10804  zsupcllemstep  10808  nn0gcdid0  10839  gcdaddm  10842  gcdadd  10843  gcdid  10844  gcdabs  10846  modgcd  10849  1gcd  10850  bezout  10867  dfgcd2  10870  mulgcd  10872  absmulgcd  10873  gcdmultiple  10876  gcdmultiplez  10877  rpmulgcd  10882  rplpwr  10883  rppwr  10884  dvdssqlem  10886  ialgr0  10893  ialginv  10896  ialgcvg  10897  ialgfx  10901  eucalginv  10905  eucalglt  10906  lcmcl  10921  lcmabs  10925  lcmgcdlem  10926  lcmdvds  10928  lcmgcdnn  10931  coprmdvds  10941  qredeq  10945  divgcdcoprm0  10950  divgcdcoprmex  10951  rpexp1i  11000  sqrt2irrlem  11007  sqpweven  11020  2sqpwodd  11021  sqrt2irraplemnn  11024  qmuldeneqnum  11040  nn0gcdsq  11045  numdensq  11047  nn0sqrtelqelz  11051  phibndlem  11059  dfphi2  11063  phiprmpw  11065  phiprm  11066  phimullem  11068  hashgcdlem  11070  djucllem  11130  nninfalllemn  11328  nninfsellemeq  11336  qdencn  11345
  Copyright terms: Public domain W3C validator