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

Theorem eqtr4d 2153
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 2123 . 2  |-  ( ph  ->  B  =  C )
41, 3eqtrd 2150 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:  3eqtr2d  2156  3eqtr2rd  2157  3eqtr4d  2160  3eqtr4rd  2161  3eqtr4a  2176  sbnfc2  3030  ifsbdc  3456  ifeq1dadc  3472  eqifdc  3476  ifandc  3478  onsucuni2  4449  relop  4659  riinint  4770  iotauni  5070  fniinfv  5447  fsn2  5562  fmptapd  5579  fconst2g  5603  fniunfv  5631  ofres  5964  ofco  5968  frecsuclem  6271  frecrdg  6273  oasuc  6328  nnacom  6348  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  funresdfunsndc  6370  uniqs2  6457  en1bg  6662  fundmen  6668  1domsn  6681  mapxpen  6710  xpmapenlem  6711  phplem4dom  6724  en2eqpr  6769  sbthlemi5  6817  omp1eomlem  6947  difinfsnlem  6952  ctmlemr  6961  ctssdccl  6964  ctssdc  6966  infnninf  6990  exmidonfinlem  7017  addcmpblnq  7143  distrnqg  7163  ltexnqq  7184  addcmpblnq0  7219  nqnq0a  7230  nqnq0m  7231  nq0m0r  7232  nq0a0  7233  nnanq0  7234  distrnq0  7235  prarloclemlo  7270  prarloclemcalc  7278  genpassl  7300  genpassu  7301  ltsosr  7540  0idsr  7543  1idsr  7544  mulextsr1lem  7556  cnegex  7908  subsub3  7962  subadd4  7974  mulneg12  8127  mulsub  8131  apreap  8316  cru  8331  recextlem1  8379  cju  8683  halfaddsub  8912  nn0supp  8987  nneo  9112  zeo2  9115  uzin  9314  xaddcom  9599  xaddass  9607  xleaddadd  9625  iccf1o  9742  fzsuc2  9814  flqeqceilz  10046  zmod1congr  10069  modqcyc  10087  modqcyc2  10088  modqaddabs  10090  modqmul1  10105  modqaddmulmod  10119  addmodlteq  10126  frec2uzrdg  10137  frecuzrdgsuctlem  10151  seq3val  10186  seqvalcd  10187  seq3fveq2  10197  seq3split  10207  seq3distr  10241  ser0f  10243  expp1  10255  mulexp  10287  mulexpzap  10288  expadd  10290  expaddzap  10292  expmul  10293  expmulzap  10294  expsubap  10296  expdivap  10299  subsq  10354  mulbinom2  10363  binom3  10364  bernneq  10367  nn0opthd  10423  faclbnd  10442  faclbnd6  10445  bccmpl  10455  bcp1n  10462  zfz1isolemiso  10537  seq3coll  10540  shftval2  10553  shftval4  10555  seq3shft  10565  crre  10584  remim  10587  remullem  10598  cjexp  10620  cnrecnv  10637  resqrexlemlo  10740  resqrexlemcalc1  10741  resqrexlemcalc2  10742  resqrexlemcalc3  10743  resqrexlemnm  10745  rsqrmo  10754  abscj  10779  absid  10798  absre  10804  recvalap  10824  maxabsle  10931  maxltsup  10945  2zsupmax  10952  minabs  10962  bdtrilem  10965  bdtri  10966  xrmaxiflemab  10971  xrmaxiflemcom  10973  xrmaxadd  10985  xrbdtri  11000  iooinsup  11001  climaddc1  11053  climmulc2  11055  climsubc1  11056  climsubc2  11057  climcvg1nlem  11073  summodclem3  11104  zsumdc  11108  isum  11109  isumz  11113  isumss  11115  fisumss  11116  fsum3cvg2  11118  fsumadd  11130  isummulc2  11150  sumsplitdc  11156  fsum2dlemstep  11158  fisumcom2  11162  fisum0diag2  11171  fsumconst  11178  telfsumo  11190  fsumparts  11194  fsumrelem  11195  binomlem  11207  isumshft  11214  isumsplit  11215  arisum  11222  arisum2  11223  trireciplem  11224  geolim2  11236  geo2sum  11238  0.999...  11245  cvgratz  11256  mertensabs  11261  ef0lem  11280  efval2  11285  ege2le3  11291  efaddlem  11294  efsub  11301  eftlub  11310  efsep  11311  tanval3ap  11335  efi4p  11338  sinneg  11347  sinmul  11365  sincossq  11369  cos2t  11371  demoivreALT  11394  eirraplem  11395  odd2np1  11482  omoe  11505  divalglemex  11531  divalglemeuneg  11532  divalgmod  11536  flodddiv4  11543  gcdneg  11582  gcdaddm  11584  modgcd  11591  bezoutlemnewy  11596  gcdass  11615  gcdmultiple  11620  algrp1  11639  lcmneg  11667  lcmgcdeq  11676  lcmass  11678  cncongr2  11697  prmexpb  11741  sqrt2irr  11752  2sqpwodd  11765  qnumdenbi  11781  phiprmpw  11809  ctiunctlemfo  11863  strslfv3  11915  restuni2  12257  lmfval  12272  cnfval  12274  cnpfval  12275  txtopon  12342  txcnp  12351  upxp  12352  txrest  12356  cnmptcom  12378  bl2in  12483  xblss2  12485  isxms2  12532  setsmsdsg  12560  setsmstsetg  12561  metss  12574  resubmet  12628  cncfcncntop  12660  dvidlemap  12740  dvcnp2cntop  12743  dvcoapbr  12751  dvcjbr  12752  dvexp  12755  dvexp2  12756  dvrecap  12757  efimpi  12811  0nninf  13093  nninfalllemn  13098  trilpolemisumle  13127
  Copyright terms: Public domain W3C validator