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

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

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
21eqcomd 2090 . 2  |-  ( ph  ->  B  =  A )
3 eqtr3d.2 . 2  |-  ( ph  ->  A  =  C )
42, 3eqtrd 2117 1  |-  ( ph  ->  B  =  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:  3eqtr3d  2125  3eqtr3rd  2126  3eqtr3a  2141  opth  4036  eusvnf  4247  f00  5158  f1imacnv  5226  foimacnv  5227  f1ococnv1  5238  funfvdm  5323  fvmptdf  5346  fndmdif  5360  acexmidlemph  5599  acexmidlemab  5600  ovmpt2df  5726  oprssov  5736  grpridd  5791  tfrlemisucaccv  6037  tfr1onlemsucaccv  6053  tfrcllemsucaccv  6066  oav2  6171  omv2  6173  ecopovtrn  6334  ecopovtrng  6337  map0b  6389  en1  6461  ssenen  6512  fidifsnen  6531  dif1en  6540  undifdc  6579  ordiso2  6664  finomni  6732  exmidomni  6734  fodjuomnilemm  6737  distrnqg  6882  1qec  6883  prarloclemarch2  6914  nnnq0lem1  6941  nqpnq0nq  6948  distrnq0  6954  prarloclemlt  6988  prmuloclemcalc  7060  ltaprg  7114  prplnqu  7115  recexprlem1ssl  7128  recexprlem1ssu  7129  ltmprr  7137  cauappcvgprlemopl  7141  caucvgprlemopl  7164  caucvgprprlemopl  7192  caucvgprprlemexb  7202  prsrlem1  7224  ltsosr  7246  mulgt0sr  7259  recidpipr  7329  recriota  7361  nntopi  7365  axcaucvglemres  7370  addid2  7557  readdcan  7558  muladd11r  7574  add32r  7578  cnegexlem2  7594  cnegex  7596  pncan2  7625  addsubass  7628  subadd23  7630  addsub12  7631  subid  7637  subid1  7638  npncan  7639  nppcan3  7642  subsub  7648  nppcan2  7649  nnncan2  7655  npncan3  7656  pnpcan  7657  negdi  7675  mvlraddd  7781  pnpncand  7789  subdi  7799  mulsub  7815  mulsub2  7816  recexap  8053  div32ap  8090  divsubdirap  8106  divmuldivap  8110  divdivdivap  8111  divmuleqap  8115  divcanap6  8117  dmdcanap  8120  divsubdivap  8126  div2negap  8133  mvllmulapd  8231  prodgt0gt0  8239  cju  8348  zneo  8772  infrenegsupex  9006  qreccl  9051  fzosn  9536  modqid  9676  modqm1p1mod0  9702  modqltm1p1mod  9703  modqmul1  9704  modaddmodup  9714  modaddmodlo  9715  modqsubdir  9720  iseqf1olemkle  9809  iseqf1olemklt  9810  iseqf1olemstep  9826  iseqf1oleml  9828  iseqdistr  9838  expineg2  9854  expm1t  9873  expadd  9887  expaddzaplem  9888  expmulzap  9891  sqsubswap  9905  subsq2  9951  binom2sub  9956  binom3  9959  facndiv  10035  ibcval5  10059  bcn2p1  10066  bcnm1  10068  2shfti  10153  shftcan2  10157  reim0  10182  imval2  10215  cjreim2  10225  cjdivap  10230  cnrecnv  10231  rennim  10322  resqrexlemnm  10338  remsqsqrt  10352  sqrtdiv  10362  sqrtmsq  10365  sqabsadd  10375  sqabssub  10376  absreim  10388  absdivap  10390  absnid  10393  sqabs  10402  abslt  10408  absle  10409  recvalap  10417  abssub  10421  maxabslemlub  10527  mulcn2  10585  cjcn2  10588  isummolem3  10651  isummolem2a  10652  isummo  10654  zisum  10655  fisum  10657  muldvds1  10687  dvdsexp  10728  oexpneg  10743  divalglemqt  10785  divalglemeunn  10787  divalglemeuneg  10789  divalgmod  10793  flodddiv4t2lthalf  10803  gcdid0  10837  gcdaddm  10841  rpmulgcd  10881  sqgcd  10884  ialgcvg  10896  eucialgcvga  10906  eucialg  10907  dvdslcm  10917  lcmeq0  10919  lcmgcd  10926  qredeu  10945  sqnprm  10983  divgcdodd  10988  sqrt2irrlem  11006  sqpweven  11019  2sqpwodd  11020  divnumden  11040  hashdvds  11063  phimullem  11067  peano3nninf  11326  nninfsel  11338
  Copyright terms: Public domain W3C validator