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

Theorem eqtr4d 2151
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr4d.1  |-  ( ph  ->  A  =  B )
eqtr4d.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
eqtr4d  |-  ( ph  ->  A  =  C )

Proof of Theorem eqtr4d
StepHypRef Expression
1 eqtr4d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqtr4d.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2121 . 2  |-  ( ph  ->  B  =  C )
41, 3eqtrd 2148 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  3eqtr2d  2154  3eqtr2rd  2155  3eqtr4d  2158  3eqtr4rd  2159  3eqtr4a  2174  sbnfc2  3028  ifsbdc  3454  ifeq1dadc  3470  eqifdc  3474  ifandc  3476  onsucuni2  4447  relop  4657  riinint  4768  iotauni  5068  fniinfv  5445  fsn2  5560  fmptapd  5577  fconst2g  5601  fniunfv  5629  ofres  5962  ofco  5966  frecsuclem  6269  frecrdg  6271  oasuc  6326  nnacom  6346  nnaass  6347  nndi  6348  nnmass  6349  nnmsucr  6350  nnmcom  6351  funresdfunsndc  6368  uniqs2  6455  en1bg  6660  fundmen  6666  1domsn  6679  mapxpen  6708  xpmapenlem  6709  phplem4dom  6722  en2eqpr  6767  sbthlemi5  6815  omp1eomlem  6945  difinfsnlem  6950  ctmlemr  6959  ctssdccl  6962  ctssdc  6964  infnninf  6988  addcmpblnq  7139  distrnqg  7159  ltexnqq  7180  addcmpblnq0  7215  nqnq0a  7226  nqnq0m  7227  nq0m0r  7228  nq0a0  7229  nnanq0  7230  distrnq0  7231  prarloclemlo  7266  prarloclemcalc  7274  genpassl  7296  genpassu  7297  ltsosr  7536  0idsr  7539  1idsr  7540  mulextsr1lem  7552  cnegex  7904  subsub3  7958  subadd4  7970  mulneg12  8123  mulsub  8127  apreap  8312  cru  8327  recextlem1  8375  cju  8679  halfaddsub  8908  nn0supp  8983  nneo  9108  zeo2  9111  uzin  9310  xaddcom  9595  xaddass  9603  xleaddadd  9621  iccf1o  9738  fzsuc2  9810  flqeqceilz  10042  zmod1congr  10065  modqcyc  10083  modqcyc2  10084  modqaddabs  10086  modqmul1  10101  modqaddmulmod  10115  addmodlteq  10122  frec2uzrdg  10133  frecuzrdgsuctlem  10147  seq3val  10182  seqvalcd  10183  seq3fveq2  10193  seq3split  10203  seq3distr  10237  ser0f  10239  expp1  10251  mulexp  10283  mulexpzap  10284  expadd  10286  expaddzap  10288  expmul  10289  expmulzap  10290  expsubap  10292  expdivap  10295  subsq  10350  mulbinom2  10359  binom3  10360  bernneq  10363  nn0opthd  10419  faclbnd  10438  faclbnd6  10441  bccmpl  10451  bcp1n  10458  zfz1isolemiso  10533  seq3coll  10536  shftval2  10549  shftval4  10551  seq3shft  10561  crre  10580  remim  10583  remullem  10594  cjexp  10616  cnrecnv  10633  resqrexlemlo  10736  resqrexlemcalc1  10737  resqrexlemcalc2  10738  resqrexlemcalc3  10739  resqrexlemnm  10741  rsqrmo  10750  abscj  10775  absid  10794  absre  10800  recvalap  10820  maxabsle  10927  maxltsup  10941  2zsupmax  10948  minabs  10958  bdtrilem  10961  bdtri  10962  xrmaxiflemab  10967  xrmaxiflemcom  10969  xrmaxadd  10981  xrbdtri  10996  iooinsup  10997  climaddc1  11049  climmulc2  11051  climsubc1  11052  climsubc2  11053  climcvg1nlem  11069  summodclem3  11100  zsumdc  11104  isum  11105  isumz  11109  isumss  11111  fisumss  11112  fsum3cvg2  11114  fsumadd  11126  isummulc2  11146  sumsplitdc  11152  fsum2dlemstep  11154  fisumcom2  11158  fisum0diag2  11167  fsumconst  11174  telfsumo  11186  fsumparts  11190  fsumrelem  11191  binomlem  11203  isumshft  11210  isumsplit  11211  arisum  11218  arisum2  11219  trireciplem  11220  geolim2  11232  geo2sum  11234  0.999...  11241  cvgratz  11252  mertensabs  11257  ef0lem  11276  efval2  11281  ege2le3  11287  efaddlem  11290  efsub  11297  eftlub  11306  efsep  11307  tanval3ap  11331  efi4p  11334  sinneg  11343  sinmul  11361  sincossq  11365  cos2t  11367  demoivreALT  11389  eirraplem  11390  odd2np1  11477  omoe  11500  divalglemex  11526  divalglemeuneg  11527  divalgmod  11531  flodddiv4  11538  gcdneg  11577  gcdaddm  11579  modgcd  11586  bezoutlemnewy  11591  gcdass  11610  gcdmultiple  11615  algrp1  11634  lcmneg  11662  lcmgcdeq  11671  lcmass  11673  cncongr2  11692  prmexpb  11736  sqrt2irr  11747  2sqpwodd  11760  qnumdenbi  11776  phiprmpw  11804  ctiunctlemfo  11858  strslfv3  11910  restuni2  12252  lmfval  12267  cnfval  12269  cnpfval  12270  txtopon  12337  txcnp  12346  upxp  12347  txrest  12351  cnmptcom  12373  bl2in  12478  xblss2  12480  isxms2  12527  setsmsdsg  12555  setsmstsetg  12556  metss  12569  resubmet  12623  cncfcncntop  12655  dvidlemap  12735  dvcnp2cntop  12738  dvcoapbr  12746  dvcjbr  12747  dvexp  12750  dvexp2  12751  dvrecap  12752  0nninf  13031  nninfalllemn  13036  trilpolemisumle  13065
  Copyright terms: Public domain W3C validator