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

Theorem eqtr3d 2147
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 2118 . 2 (𝜑𝐵 = 𝐴)
3 eqtr3d.2 . 2 (𝜑𝐴 = 𝐶)
42, 3eqtrd 2145 1 (𝜑𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-cleq 2106
This theorem is referenced by:  3eqtr3d  2153  3eqtr3rd  2154  3eqtr3a  2169  opth  4117  eusvnf  4332  f00  5270  f1imacnv  5338  foimacnv  5339  f1ococnv1  5350  funfvdm  5436  fvmptdf  5460  fndmdif  5477  acexmidlemph  5719  acexmidlemab  5720  ovmpodf  5854  oprssov  5864  grpridd  5919  tfrlemisucaccv  6174  tfr1onlemsucaccv  6190  tfrcllemsucaccv  6203  oav2  6311  omv2  6313  fnsnsplitdc  6353  ecopovtrn  6478  ecopovtrng  6481  map0b  6533  en1  6645  ssenen  6696  fidifsnen  6715  dif1en  6724  undifdc  6763  fidcenumlemr  6793  ordiso2  6870  finomni  6960  exmidomni  6962  fodjum  6966  exmidaclem  7009  distrnqg  7137  1qec  7138  prarloclemarch2  7169  nnnq0lem1  7196  nqpnq0nq  7203  distrnq0  7209  prarloclemlt  7243  prmuloclemcalc  7315  ltaprg  7369  prplnqu  7370  recexprlem1ssl  7383  recexprlem1ssu  7384  ltmprr  7392  cauappcvgprlemopl  7396  caucvgprlemopl  7419  caucvgprprlemopl  7447  caucvgprprlemexb  7457  prsrlem1  7479  ltsosr  7501  mulgt0sr  7514  recidpipr  7585  recriota  7619  nntopi  7623  axcaucvglemres  7628  addid2  7818  readdcan  7819  muladd11r  7835  add32r  7839  cnegexlem2  7855  cnegex  7857  pncan2  7886  addsubass  7889  subadd23  7891  addsub12  7892  subid  7898  subid1  7899  npncan  7900  nppcan3  7903  subsub  7909  nppcan2  7910  nnncan2  7916  npncan3  7917  pnpcan  7918  negdi  7936  mvlraddd  8042  pnpncand  8050  subdi  8060  mulsub  8076  mulsub2  8077  eqord1  8158  recexap  8321  div32ap  8359  divsubdirap  8375  divmuldivap  8379  divdivdivap  8380  divmuleqap  8384  divcanap6  8386  dmdcanap  8389  divsubdivap  8395  div2negap  8402  div2subap  8503  mvllmulapd  8505  prodgt0gt0  8513  cju  8623  zneo  9050  infrenegsupex  9285  qreccl  9330  xnpcan  9542  fzosn  9869  modqid  10009  modqm1p1mod0  10035  modqltm1p1mod  10036  modqmul1  10037  modaddmodup  10047  modaddmodlo  10048  modqsubdir  10053  iseqf1olemkle  10144  iseqf1olemklt  10145  seq3f1olemstep  10161  seq3f1oleml  10163  seqfeq3  10172  seq3distr  10173  expineg2  10189  expm1t  10208  expadd  10222  expaddzaplem  10223  expmulzap  10226  sqsubswap  10240  subsq2  10287  binom2sub  10292  binom3  10296  facndiv  10372  bcval5  10396  bcn2p1  10403  bcnm1  10405  2shfti  10490  shftcan2  10494  reim0  10520  imval2  10553  cjreim2  10563  cjdivap  10568  cnrecnv  10569  rennim  10660  resqrexlemnm  10676  remsqsqrt  10690  sqrtdiv  10700  sqrtmsq  10703  sqabsadd  10713  sqabssub  10714  absreim  10726  absdivap  10728  absnid  10731  sqabs  10740  abslt  10746  absle  10747  recvalap  10755  abssub  10759  maxabslemlub  10865  infxrnegsupex  10918  mulcn2  10967  reccn2ap  10968  cjcn2  10971  summodclem3  11035  summodclem2a  11036  summodc  11038  zsumdc  11039  fsum3  11042  fisumss  11047  fsumcl2lem  11053  fsumm1  11071  fsum1p  11073  isummulc2  11081  telfsumo  11121  binomlem  11138  bcxmas  11144  arisum  11153  trireciplem  11155  trirecip  11156  geolim2  11167  georeclim  11168  cvgratnnlemfm  11184  cvgratz  11187  mertenslemi1  11190  efcan  11227  efexp  11233  efzval  11234  efgt0  11235  eftlub  11241  efltim  11249  resinval  11267  recosval  11268  cosmul  11297  cos2t  11302  cos2tsin  11303  cos01bnd  11310  eirraplem  11325  muldvds1  11360  dvdsexp  11401  oexpneg  11416  divalglemqt  11458  divalglemeunn  11460  divalglemeuneg  11462  divalgmod  11466  flodddiv4t2lthalf  11476  gcdid0  11510  gcdaddm  11514  rpmulgcd  11554  sqgcd  11557  algcvg  11569  eucalgcvga  11579  eucalg  11580  dvdslcm  11590  lcmeq0  11592  lcmgcd  11599  qredeu  11618  sqnprm  11656  divgcdodd  11661  sqrt2irrlem  11679  sqpweven  11692  2sqpwodd  11693  divnumden  11713  hashdvds  11736  phimullem  11740  ennnfonelemhf1o  11765  strslssd  11842  topnidg  11970  restopnb  12187  txcnmpt  12278  cnmpt1t  12290  blhalf  12391  xmspropd  12460  mspropd  12461  limcimolemlt  12583  peano3nninf  12882  nninfsel  12894  nninffeq  12897  isomninnlem  12906  cvgcmp2nlemabs  12908  trilpolemlt1  12915
  Copyright terms: Public domain W3C validator