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

Theorem eqtr3d 2119
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 2090 . 2 (𝜑𝐵 = 𝐴)
3 eqtr3d.2 . 2 (𝜑𝐴 = 𝐶)
42, 3eqtrd 2117 1 (𝜑𝐵 = 𝐶)
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  4040  eusvnf  4251  f00  5167  f1imacnv  5235  foimacnv  5236  f1ococnv1  5247  funfvdm  5332  fvmptdf  5355  fndmdif  5369  acexmidlemph  5608  acexmidlemab  5609  ovmpt2df  5735  oprssov  5745  grpridd  5800  tfrlemisucaccv  6046  tfr1onlemsucaccv  6062  tfrcllemsucaccv  6075  oav2  6180  omv2  6182  ecopovtrn  6343  ecopovtrng  6346  map0b  6398  en1  6470  ssenen  6521  fidifsnen  6540  dif1en  6549  undifdc  6588  ordiso2  6675  finomni  6743  exmidomni  6745  fodjuomnilemm  6748  distrnqg  6893  1qec  6894  prarloclemarch2  6925  nnnq0lem1  6952  nqpnq0nq  6959  distrnq0  6965  prarloclemlt  6999  prmuloclemcalc  7071  ltaprg  7125  prplnqu  7126  recexprlem1ssl  7139  recexprlem1ssu  7140  ltmprr  7148  cauappcvgprlemopl  7152  caucvgprlemopl  7175  caucvgprprlemopl  7203  caucvgprprlemexb  7213  prsrlem1  7235  ltsosr  7257  mulgt0sr  7270  recidpipr  7340  recriota  7372  nntopi  7376  axcaucvglemres  7381  addid2  7568  readdcan  7569  muladd11r  7585  add32r  7589  cnegexlem2  7605  cnegex  7607  pncan2  7636  addsubass  7639  subadd23  7641  addsub12  7642  subid  7648  subid1  7649  npncan  7650  nppcan3  7653  subsub  7659  nppcan2  7660  nnncan2  7666  npncan3  7667  pnpcan  7668  negdi  7686  mvlraddd  7792  pnpncand  7800  subdi  7810  mulsub  7826  mulsub2  7827  recexap  8064  div32ap  8101  divsubdirap  8117  divmuldivap  8121  divdivdivap  8122  divmuleqap  8126  divcanap6  8128  dmdcanap  8131  divsubdivap  8137  div2negap  8144  mvllmulapd  8242  prodgt0gt0  8250  cju  8359  zneo  8783  infrenegsupex  9017  qreccl  9062  fzosn  9547  modqid  9687  modqm1p1mod0  9713  modqltm1p1mod  9714  modqmul1  9715  modaddmodup  9725  modaddmodlo  9726  modqsubdir  9731  iseqf1olemkle  9837  iseqf1olemklt  9838  iseqf1olemstep  9854  iseqf1oleml  9856  iseqdistr  9866  ser0  9869  ser0f  9870  ser3le  9873  expineg2  9884  expm1t  9903  expadd  9917  expaddzaplem  9918  expmulzap  9921  sqsubswap  9935  subsq2  9981  binom2sub  9986  binom3  9989  facndiv  10065  ibcval5  10089  bcn2p1  10096  bcnm1  10098  2shfti  10183  shftcan2  10187  reim0  10212  imval2  10245  cjreim2  10255  cjdivap  10260  cnrecnv  10261  rennim  10352  resqrexlemnm  10368  remsqsqrt  10382  sqrtdiv  10392  sqrtmsq  10395  sqabsadd  10405  sqabssub  10406  absreim  10418  absdivap  10420  absnid  10423  sqabs  10432  abslt  10438  absle  10439  recvalap  10447  abssub  10451  maxabslemlub  10557  mulcn2  10617  cjcn2  10620  isummolem3  10683  isummolem2a  10684  isummo  10686  zisum  10687  fisum  10689  fisumss  10694  fsumcl2lem  10699  fsumm1  10716  fsum1p  10718  muldvds1  10746  dvdsexp  10787  oexpneg  10802  divalglemqt  10844  divalglemeunn  10846  divalglemeuneg  10848  divalgmod  10852  flodddiv4t2lthalf  10862  gcdid0  10896  gcdaddm  10900  rpmulgcd  10940  sqgcd  10943  ialgcvg  10955  eucialgcvga  10965  eucialg  10966  dvdslcm  10976  lcmeq0  10978  lcmgcd  10985  qredeu  11004  sqnprm  11042  divgcdodd  11047  sqrt2irrlem  11065  sqpweven  11078  2sqpwodd  11079  divnumden  11099  hashdvds  11122  phimullem  11126  peano3nninf  11385  nninfsel  11397
  Copyright terms: Public domain W3C validator