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

Theorem eqtrd 2150
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 2129 . 2  |-  ( ph  ->  ( A  =  B  <-> 
A  =  C ) )
41, 3mpbid 146 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqtr2d  2151  eqtr3d  2152  eqtr4d  2153  3eqtrd  2154  3eqtrrd  2155  3eqtr2d  2156  syl5eq  2162  syl6eq  2166  rabeqbidv  2655  rabeqbidva  2656  csbidmg  3026  csbco3g  3028  difeq12d  3165  ifeq12d  3461  ifbieq1d  3464  ifbieq2d  3466  ifbieq12d  3468  eqifdc  3476  csbsng  3554  disjpr2  3557  csbunig  3714  iuneq12d  3807  unisn3  4336  op1stbg  4370  opthreg  4441  onsucuni2  4449  csbxpg  4590  coeq12d  4673  csbdmg  4703  reseq12d  4790  csbresg  4792  resima2  4823  imaeq12d  4852  csbrng  4970  opswapg  4995  relcnvtr  5028  relcoi2  5039  relcoi1  5040  iotaint  5071  funprg  5143  funtpg  5144  funcnvres2  5168  fnco  5201  fococnv2  5361  fveq12d  5396  csbfv12g  5425  csbfv2g  5426  csbfvg  5427  dffn5im  5435  funfvdm2  5453  fvun1  5455  fvmpt2d  5475  fvmptt  5480  fndmin  5495  fniniseg2  5510  fnniniseg2  5511  fmptcof  5555  fvresi  5581  fvunsng  5582  fvpr1g  5594  fvpr2g  5595  fvtp1g  5596  funiunfvdm  5632  fcof1o  5658  riotaeqbidv  5701  oveq123d  5763  csbov12g  5778  csbov1g  5779  csbov2g  5780  ovmpodxf  5864  caov42d  5925  caovdilemd  5930  caovimo  5932  grprinvd  5934  offeq  5963  offval2  5965  caofinvl  5972  ot1stg  6018  ot2ndg  6019  2nd1st  6046  mpomptsx  6063  dmmpossx  6065  fmpox  6066  fmpoco  6081  1stconst  6086  algrflemg  6095  tfrexlem  6199  rdgivallem  6246  rdgisuc1  6249  frec0g  6262  frecabcl  6264  frecsuclem  6271  frecrdg  6273  oa0  6321  oasuc  6328  oa1suc  6331  omsuc  6336  nnaass  6349  nndi  6350  nnmass  6351  nnm2  6389  nn2m  6390  ereq1  6404  errn  6419  uniqs2  6457  oviec  6503  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  mapsnconst  6556  mapen  6708  mapxpen  6710  xpmapenlem  6711  phplem4on  6729  fidifsnen  6732  undifdc  6780  fiintim  6785  fisseneq  6788  snexxph  6806  sbthlemi4  6816  sbthlemi6  6818  supeq2  6844  eqsupti  6851  infvalti  6877  djuf1olem  6906  djuss  6923  1stinl  6927  2ndinl  6928  1stinr  6929  2ndinr  6930  updjudhcoinlf  6933  updjudhcoinrg  6934  omp1eomlem  6947  difinfsn  6953  ctmlemr  6961  ctssdclemn0  6963  ctssdc  6966  enumctlemm  6967  en2other2  7020  mulidpi  7094  addasspig  7106  mulasspig  7108  distrpig  7109  indpi  7118  addcmpblnq  7143  mulpipq  7148  dmaddpqlem  7153  nqpi  7154  addcomnqg  7157  recrecnq  7170  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltaddnq  7183  ltexnqq  7184  archnqq  7193  prarloclemarch  7194  ltrnqg  7196  ltnnnq  7199  nq0nn  7218  addcmpblnq0  7219  nqpnq0nq  7229  nqnq0a  7230  nq0m0r  7232  nq0a0  7233  distrnq0  7235  addassnq0  7238  nq02m  7241  prarloclemlo  7270  prarloclemcalc  7278  addnqprllem  7303  addnqprulem  7304  addnqprl  7305  addnqpru  7306  appdivnq  7339  mulnqprl  7344  mulnqpru  7345  addcanprlemu  7391  ltaprlem  7394  ltmprr  7418  cauappcvgprlemladdrl  7433  mulcmpblnrlemg  7516  mulcomsrg  7533  distrsrg  7535  ltsosr  7540  1idsr  7544  00sr  7545  ltasrg  7546  recexgt0sr  7549  srpospr  7559  prsradd  7562  prsrriota  7564  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsrlemoffres  7576  caucvgsr  7578  map2psrprg  7581  elreal2  7606  mulresr  7614  pitonnlem1p1  7622  pitonnlem2  7623  pitoregt0  7625  recidpirqlemcalc  7633  recidpirq  7634  axaddcl  7640  axmulcl  7642  axmulcom  7647  axmulass  7649  axdistr  7650  ax1rid  7653  axcnre  7657  recriota  7666  axcaucvglemcau  7674  mulid1  7731  mulid2  7732  adddirp1d  7760  joinlmuladdmuld  7761  muladd11  7863  1p1times  7864  readdcan  7870  comraddd  7887  add42  7892  npcan  7939  addsubass  7940  2addsub  7944  addsubeq4  7945  nppcan  7952  nnpcan  7953  npncan2  7957  nncan  7959  subsub  7960  nnncan  7965  nnncan1  7966  pnpcan2  7970  pnncan  7971  subneg  7979  negneg  7980  negdi2  7988  mvrraddd  8096  assraddsubd  8098  subaddeqd  8099  addid0  8103  mul02  8117  mul01  8119  mulneg1  8125  mul2neg  8128  mulm1  8130  ltadd2  8149  rimul  8315  rereim  8316  mulreim  8334  recextlem1  8380  mulcanapd  8390  divcanap1  8409  divrecap2  8417  divmulassap  8423  divmulasscomap  8424  divcanap4  8427  dividap  8429  muldivdirap  8435  divdivdivap  8441  recdivap  8446  divadddivap  8455  divsubdivap  8456  div2negap  8463  divcanap5rd  8546  dmdcanap2d  8549  subrecap  8566  recgt0  8576  lt2mul2div  8605  nnmulcl  8709  times2  8817  add1p1  8937  sub1m1  8938  cnm2m1cnm3  8939  nn0supp  8997  peano2z  9058  nneoor  9121  supminfex  9360  cnref1o  9408  rexneg  9581  xaddpnf1  9597  xaddmnf1  9599  rexadd  9603  xaddid1  9613  xaddid2  9614  xaddass  9620  xpncan  9622  xleadd1a  9624  xltadd1  9627  xposdif  9633  xadd4d  9636  xleaddadd  9638  iooidg  9660  iooval2  9666  icoshftf1o  9742  lincmb01cmp  9754  iccf1o  9755  fzval2  9761  fzsuc  9817  fzpred  9818  fztpval  9831  fseq1p1m1  9842  fzshftral  9856  fzo0to3tp  9964  fzo0sn0fzo1  9966  fzosplitsn  9978  fzosplitprm1  9979  fzisfzounsn  9981  rebtwn2zlemstep  9998  2tnp1ge0ge0  10042  flqdiv  10062  modqvalr  10066  modqdiffl  10076  modqfrac  10078  modqmulnn  10083  modqid  10090  modqcyc  10100  modqcyc2  10101  mulp1mod1  10106  modqmuladd  10107  modqmuladdnn0  10109  qnegmod  10110  m1modnnsub1  10111  addmodid  10113  addmodidr  10114  modqmul12d  10119  modqnegd  10120  modqadd12d  10121  modifeq2int  10127  modqaddmulmod  10132  modqdi  10133  modqsubdir  10134  modsumfzodifsn  10137  addmodlteq  10139  frec2uzsucd  10142  frecuzrdgrrn  10149  frec2uzrdg  10150  frecuzrdglem  10152  frecuzrdgsuc  10155  frecuzrdgg  10157  frecuzrdgdomlem  10158  frecuzrdgfunlem  10160  frecuzrdgtclt  10162  frecuzrdgsuctlem  10164  frecfzennn  10167  seqeq1  10189  seq3val  10199  seqvalcd  10200  seq3p1  10203  seqp1cd  10207  seq3feq2  10211  seq3fveq  10212  seq3shft2  10214  seq3-1p  10221  iseqf1olemnab  10229  iseqf1olemab  10230  iseqf1olemnanb  10231  iseqf1olemqk  10235  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3f1olemqsum  10241  seq3f1o  10245  seq3id3  10248  seq3z  10252  fser0const  10257  exp3vallem  10262  expnnval  10264  expp1  10268  expn1ap0  10271  mulexp  10300  expaddzaplem  10304  expaddzap  10305  expmul  10306  expp1zap  10310  expm1ap  10311  sqval  10319  iexpcyc  10365  subsq2  10368  binom2  10371  binom21  10372  binom2sub1  10374  mulbinom2  10376  binom3  10377  zesq  10378  bernneq  10380  sqoddm1div8  10412  nn0opthlem1d  10434  facp1  10444  faclbnd6  10458  bcval2  10464  bcval3  10465  bcn0  10469  bcp1n  10475  bcp1nk  10476  bcn2  10478  bcp1m1  10479  bcpasc  10480  bcn2m1  10483  hashinfom  10492  hashennn  10494  hashfz1  10497  fseq1hash  10515  omgadd  10516  hashunsng  10521  hashprg  10522  hashdifsn  10533  hashdifpr  10534  hashfz  10535  hashfzo  10536  hashfzo0  10537  hashfzp1  10538  hashfz0  10539  hashxp  10540  resunimafz0  10542  fnfz0hash  10543  ffzo0hash  10545  hashfacen  10547  zfz1isolemsplit  10549  zfz1isolemiso  10550  zfz1isolem1  10551  shftdm  10562  shftval2  10566  shftval4  10568  shftval5  10569  shftcan1  10574  seq3shft  10578  imre  10591  crre  10597  remim  10600  reim0b  10602  recj  10607  reneg  10608  readd  10609  resub  10610  remullem  10611  imcj  10615  imneg  10616  imadd  10617  imsub  10618  cjcj  10623  cjadd  10624  ipcnval  10626  cjneg  10630  cjsub  10632  cjexp  10633  imval2  10634  cjap  10646  resqrexlemf1  10748  resqrexlemfp1  10749  resqrexlemover  10750  resqrexlemcalc1  10754  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemcvg  10759  resqrtcl  10769  sqrtsq  10784  absneg  10790  absvalsq  10793  absvalsq2  10794  sqabsadd  10795  sqabssub  10796  absval2  10797  absreimsq  10807  absmul  10809  absexp  10819  absexpzap  10820  abssuble0  10843  abstri  10844  recan  10849  amgm2  10858  maxabslemlub  10947  max0addsup  10959  minmax  10969  minabs  10975  bdtrilem  10978  bdtri  10979  xrmaxiflemab  10984  xrmaxiflemcom  10986  xrmaxadd  10998  xrminmax  11002  xrmineqinf  11006  xrminrecl  11010  xrbdtri  11013  climshft2  11043  subcn2  11048  reccn2ap  11050  climaddc2  11067  iser3shft  11083  climcvg1nlem  11086  sumeq12dv  11109  sumeq12rdv  11110  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  summodc  11120  fsum3  11124  isumz  11126  fsumf1o  11127  fisumss  11129  fsumsersdc  11132  fsum3ser  11134  fsumsplit  11144  fsumsplitf  11145  sumsnf  11146  fsumsplitsn  11147  fsum1  11149  sumpr  11150  sumtp  11151  fsumm1  11153  fsum1p  11155  fsumsplitsnun  11156  fsump1  11157  isumclim  11158  sumnul  11161  isumadd  11168  fsum2dlemstep  11171  fsumcnv  11174  fisumcom2  11175  fsumshftm  11182  fisumrev2  11183  fisum0diag2  11184  fsumsub  11189  fsumdifsnconst  11192  modfsummodlemstep  11194  fsumabs  11202  telfsumo  11203  telfsum  11205  telfsum2  11206  fsumparts  11207  fsumiun  11214  hashiun  11215  hash2iun  11216  hash2iun1dif1  11217  binomlem  11220  binom1p  11222  binom11  11223  binom1dif  11224  bcxmas  11226  isum1p  11229  isumnn0nn  11230  isumlessdc  11233  divcnv  11234  arisum2  11236  trireciplem  11237  geosergap  11243  geolim  11248  georeclim  11250  geo2lim  11253  geoisum1  11256  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemsumlt  11265  cvgratz  11269  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  eftabs  11289  efcllemp  11291  ef0lem  11293  efcvgfsum  11300  ege2le3  11304  efcj  11306  efaddlem  11307  efexp  11315  eftlub  11323  efsep  11324  effsumlt  11325  ef4p  11327  efgt1p2  11328  efgt1p  11329  tanval2ap  11347  tanval3ap  11348  resinval  11349  recosval  11350  efi4p  11351  resin4p  11352  recos4p  11353  sinneg  11360  cosneg  11361  tannegap  11362  efmival  11367  sinadd  11370  cosadd  11371  tanaddaplem  11372  tanaddap  11373  sinsub  11374  cossub  11375  addsin  11376  subsin  11377  subcos  11381  sincossq  11382  sin2t  11383  sin01bnd  11391  cos01bnd  11392  absefi  11402  absef  11403  absefib  11404  efieq1re  11405  demoivre  11406  demoivreALT  11407  eirraplem  11410  dvdstr  11457  dvdsadd2b  11467  mulmoddvds  11488  ltoddhalfle  11517  opoe  11519  m1expo  11524  m1exp1  11525  flodddiv4  11558  flodddiv4t2lthalf  11561  zsupcllemstep  11565  nn0gcdid0  11596  gcdaddm  11599  gcdadd  11600  gcdid  11601  gcdabs  11603  modgcd  11606  1gcd  11607  bezout  11626  dfgcd2  11629  mulgcd  11631  absmulgcd  11632  gcdmultiple  11635  gcdmultiplez  11636  rpmulgcd  11641  rplpwr  11642  rppwr  11643  dvdssqlem  11645  ialgr0  11652  alginv  11655  algcvg  11656  algfx  11660  eucalginv  11664  eucalglt  11665  lcmcl  11680  lcmabs  11684  lcmgcdlem  11685  lcmdvds  11687  lcmgcdnn  11690  coprmdvds  11700  qredeq  11704  divgcdcoprm0  11709  divgcdcoprmex  11710  rpexp1i  11759  sqrt2irrlem  11766  sqpweven  11780  2sqpwodd  11781  sqrt2irraplemnn  11784  qmuldeneqnum  11800  nn0gcdsq  11805  numdensq  11807  nn0sqrtelqelz  11811  phibndlem  11819  dfphi2  11823  phiprmpw  11825  phiprm  11826  phimullem  11828  hashgcdlem  11830  ennnfonelemp1  11846  ennnfonelemhdmp1  11849  ennnfonelemss  11850  ennnfonelemkh  11852  ennnfonelemhf1o  11853  ennnfonelemhom  11855  ennnfonelemnn0  11862  ctinfomlemom  11867  setsvala  11917  fvsetsid  11920  setsresg  11924  setscom  11926  setsslid  11936  ressid2  11945  ressval2  11946  restid2  12056  ntrval  12206  clsval  12207  cldcls  12210  neival  12239  resttop  12266  restco  12270  restabs  12271  resttopon2  12274  cnpval  12294  cnntr  12321  cnrest2  12332  upxp  12368  uptx  12370  cnmpt11  12379  cnmpt21  12387  psmetsym  12425  psmetres2  12429  xmetsym  12464  xmettxlem  12605  txmetcnp  12614  cnbl0  12630  cnblcld  12631  remetdval  12635  bl2ioo  12638  tgioo  12642  addcncntoplem  12647  divcnap  12651  fsumcncntop  12652  cncfmet  12675  cncfmptc  12678  addccncf  12682  negcncf  12684  mulcncflem  12686  ivthinclemlopn  12710  limcimolemlt  12729  cnplimcim  12732  cnplimclemr  12734  limccnp2lem  12741  limccnp2cntop  12742  dvfvalap  12746  dvconst  12757  dvaddxxbr  12761  dvmulxxbr  12762  dvcjbr  12768  dvexp  12771  dvrecap  12773  dvmptclx  12776  dvmptaddx  12777  dvmptmulx  12778  dvmptcmulcn  12779  dveflem  12782  dvef  12783  sin0pilem1  12789  sin0pilem2  12790  efper  12815  sinperlem  12816  sinmpi  12823  cosmpi  12824  sinppi  12825  cosppi  12826  efimpi  12827  ptolemy  12832  sinq12gt0  12838  coseq0negpitopi  12844  tangtx  12846  abssinper  12854  cosq34lt1  12858  djucllem  12934  nninfalllemn  13129  nninfsellemeq  13137  nninffeq  13143  qdencn  13149  cvgcmp2nlemabs  13154  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator