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

Theorem eqtr3d 2116
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)
Hypotheses
Ref Expression
eqtr3d.1 (𝜑𝐴 = 𝐵)
eqtr3d.2 (𝜑𝐴 = 𝐶)
Assertion
Ref Expression
eqtr3d (𝜑𝐵 = 𝐶)

Proof of Theorem eqtr3d
StepHypRef Expression
1 eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2087 . 2 (𝜑𝐵 = 𝐴)
3 eqtr3d.2 . 2 (𝜑𝐴 = 𝐶)
42, 3eqtrd 2114 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  3eqtr3d  2122  3eqtr3rd  2123  3eqtr3a  2138  opth  4000  eusvnf  4211  f00  5112  f1imacnv  5174  foimacnv  5175  f1ococnv1  5186  funfvdm  5268  fvmptdf  5290  fndmdif  5304  acexmidlemph  5536  acexmidlemab  5537  ovmpt2df  5663  oprssov  5673  grpridd  5728  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  oav2  6107  omv2  6109  ecopovtrn  6269  ecopovtrng  6272  en1  6346  fidifsnen  6405  dif1en  6414  undiffi  6443  ordiso2  6505  distrnqg  6639  1qec  6640  prarloclemarch2  6671  nnnq0lem1  6698  nqpnq0nq  6705  distrnq0  6711  prarloclemlt  6745  prmuloclemcalc  6817  ltaprg  6871  prplnqu  6872  recexprlem1ssl  6885  recexprlem1ssu  6886  ltmprr  6894  cauappcvgprlemopl  6898  caucvgprlemopl  6921  caucvgprprlemopl  6949  caucvgprprlemexb  6959  prsrlem1  6981  ltsosr  7003  mulgt0sr  7016  recidpipr  7086  recriota  7118  nntopi  7122  axcaucvglemres  7127  addid2  7314  readdcan  7315  muladd11r  7331  add32r  7335  cnegexlem2  7351  cnegex  7353  pncan2  7382  addsubass  7385  subadd23  7387  addsub12  7388  subid  7394  subid1  7395  npncan  7396  nppcan3  7399  subsub  7405  nppcan2  7406  nnncan2  7412  npncan3  7413  pnpcan  7414  negdi  7432  mvlraddd  7538  pnpncand  7546  subdi  7556  mulsub  7572  mulsub2  7573  recexap  7810  div32ap  7847  divsubdirap  7863  divmuldivap  7867  divdivdivap  7868  divmuleqap  7872  divcanap6  7874  dmdcanap  7877  divsubdivap  7883  div2negap  7890  mvllmulapd  7988  prodgt0gt0  7996  cju  8105  zneo  8529  infrenegsupex  8763  qreccl  8808  fzosn  9291  modqid  9431  modqm1p1mod0  9457  modqltm1p1mod  9458  modqmul1  9459  modaddmodup  9469  modaddmodlo  9470  modqsubdir  9475  iseqdistr  9567  expineg2  9582  expm1t  9601  expadd  9615  expaddzaplem  9616  expmulzap  9619  sqsubswap  9633  subsq2  9679  binom2sub  9684  binom3  9687  facndiv  9763  ibcval5  9787  bcn2p1  9794  bcnm1  9796  2shfti  9857  shftcan2  9861  reim0  9886  imval2  9919  cjreim2  9929  cjdivap  9934  cnrecnv  9935  rennim  10026  resqrexlemnm  10042  remsqsqrt  10056  sqrtdiv  10066  sqrtmsq  10069  sqabsadd  10079  sqabssub  10080  absreim  10092  absdivap  10094  absnid  10097  sqabs  10106  abslt  10112  absle  10113  recvalap  10121  abssub  10125  maxabslemlub  10231  mulcn2  10289  cjcn2  10292  muldvds1  10365  dvdsexp  10406  oexpneg  10421  divalglemqt  10463  divalglemeunn  10465  divalglemeuneg  10467  divalgmod  10471  flodddiv4t2lthalf  10481  gcdid0  10515  gcdaddm  10519  rpmulgcd  10559  sqgcd  10562  ialgcvg  10574  eucialgcvga  10584  eucialg  10585  dvdslcm  10595  lcmeq0  10597  lcmgcd  10604  qredeu  10623  sqnprm  10661  divgcdodd  10666  sqrt2irrlem  10684  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator