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

Theorem eqeq1d 2126
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eqeq1d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  C ) )

Proof of Theorem eqeq1d
StepHypRef Expression
1 eqeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq1 2124 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = 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:  rspcedeq1vd  2772  sbceq2g  2995  csbhypf  3008  csbiebt  3009  csbiebg  3012  dfss4st  3279  disjssun  3396  sneqrg  3659  preq12b  3667  preq12bg  3670  disji2  3892  iin0r  4063  opthg  4130  opeqsn  4144  unisucg  4306  opthreg  4441  tfisi  4471  dmsnopg  4980  relcoi1  5040  iotaeq  5066  iotabi  5067  fneq1  5181  fnun  5199  fnresdisj  5203  fnimadisj  5213  fnimaeq0  5214  sbcfng  5240  foeq1  5311  foco  5325  fveqeq2d  5397  fvelimab  5445  fvun1  5455  fvmptdv2  5478  fneqeql  5496  dffo3  5535  fvsng  5584  fconstfvm  5606  eufnfv  5616  f1veqaeq  5638  dff13f  5639  f1elima  5642  foeqcnvco  5659  f1eqcocnv  5660  acexmidlemab  5736  ovanraleqv  5766  eloprabga  5826  ovmpodv2  5872  ovi3  5875  ovelimab  5889  caovcang  5900  caovcan  5903  caovimo  5932  grprinvlem  5933  grpridd  5935  suppssfv  5946  suppssov1  5947  caofinvl  5972  op1stg  6016  op2ndg  6017  eqop  6043  reldm  6052  xporderlem  6096  tposfo2  6132  frec0g  6262  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecsuc  6272  nnm0r  6343  nnmord  6381  nnaordex  6391  nnawordex  6392  ereq1  6404  eqerlem  6428  mapsn  6552  endisj  6686  xpf1o  6706  mapxpen  6710  fidifsnen  6732  supelti  6857  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  omp1eomlem  6947  difinfsnlem  6952  enomnilem  6978  finomni  6980  exmidomni  6982  fodjuomnilemres  6988  fodjuomni  6989  ismkvnex  6997  mkvprop  7000  fodjumkvlemres  7001  pm54.43  7014  exmidfodomrlemrALT  7027  addnidpig  7112  ltexpi  7113  dfplpq2  7130  dfmpq2  7131  recexnq  7166  recmulnqg  7167  ltexnqq  7184  halfnqq  7186  enq0tr  7210  nqnq0pi  7214  addnnnq0  7225  addlocpr  7312  ltexprlemru  7388  ltexpri  7389  lteupri  7393  prplnqu  7396  recexpr  7414  addsrpr  7521  mulsrpr  7522  00sr  7545  negexsr  7548  recexgt0sr  7549  srpospr  7559  prsrriota  7564  caucvgsrlemfv  7567  map2psrprg  7581  elrealeu  7605  axrnegex  7655  axprecex  7656  rereceu  7665  recriota  7666  nntopi  7670  axcaucvglemval  7673  axcaucvglemcau  7674  cnegexlem1  7905  cnegex  7908  cnegex2  7909  subval  7922  subadd  7933  subadd2  7934  subsub23  7935  addsubeq4  7945  subcan2  7955  negcon1  7982  subcan  7985  addrsub  8101  ltadd2  8149  ltordlem  8212  recexre  8307  recexap  8381  muleqadd  8396  receuap  8397  divvalap  8401  divmulap  8402  rec11ap  8437  zdiv  9097  uzin  9314  xaddval  9583  xnn0xadd0  9605  xnegdi  9606  xltadd1  9614  icc0r  9664  fznlem  9776  fseq1m1p1  9830  1fv  9871  fzon  9898  fvinim0ffz  9973  ioo0  9992  ico0  9994  ioc0  9995  flqbi  10018  divfl0  10024  modq0  10057  modqmuladdnn0  10096  addmodlteq  10126  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  seq3f1olemstep  10229  seq3f1olemp  10230  seq3id  10236  seq3z  10239  mulreap  10591  rennim  10729  resqrexlemex  10752  rsqrmo  10754  resqrtcl  10756  rersqrtthlem  10757  sqrtsq2  10770  isumss  11115  fsum00  11186  telfsumo  11190  pwm1geoserap1  11232  absefib  11391  efieq1re  11392  divides  11407  dvdsval2  11408  nndivides  11412  dvds0lem  11415  dvds1lem  11416  dvds2lem  11417  negdvdsb  11421  muldvds1  11430  muldvds2  11431  dvdscmulr  11434  dvdsmulcr  11435  dvdstr  11442  dvdsabseq  11457  divconjdvds  11459  odd2np1lem  11481  odd2np1  11482  even2n  11483  oddm1even  11484  2tp1odd  11493  opeo  11506  omeo  11507  m1exp1  11510  divalgb  11534  gcdaddm  11584  gcdabs1  11589  bezout  11611  gcdmultiple  11620  gcdmultiplez  11621  rplpwr  11627  rppwr  11628  alginv  11640  algcvga  11644  algfx  11645  eucalgval2  11646  coprmdvds  11685  qredeq  11689  qredeu  11690  divgcdcoprm0  11694  divgcdcoprmex  11695  cncongr1  11696  rpexp  11743  rpexp12i  11745  cncongrprm  11747  qnumdenbi  11781  phival  11800  phicl2  11801  dfphi2  11807  phiprmpw  11809  phimullem  11812  hashgcdlem  11814  ennnfonelemhf1o  11837  ntreq0  12212  ispsmet  12403  psmet0  12407  ismet  12424  isxmet  12425  xmeteq0  12439  metn0  12458  xmetres2  12459  xblss2ps  12484  xblss2  12485  xmseq0  12548  comet  12579  bdxmet  12581  cnmet  12610  ivthdec  12702  pwle2  13089  subctctexmid  13092  peano4nninf  13096  nninfalllemn  13098  nninfalllem1  13099  nninfsellemdc  13102  nninfsellemeq  13106  nninfsellemqall  13107  nninfsellemeqinf  13108  nninfomnilem  13110  nninfomni  13111  isomninnlem  13121  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator