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

Theorem eqeq1d 2124
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 2122 . 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 1314
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  rspcedeq1vd  2770  sbceq2g  2993  csbhypf  3006  csbiebt  3007  csbiebg  3010  dfss4st  3277  disjssun  3394  sneqrg  3657  preq12b  3665  preq12bg  3668  disji2  3890  iin0r  4061  opthg  4128  opeqsn  4142  unisucg  4304  opthreg  4439  tfisi  4469  dmsnopg  4978  relcoi1  5038  iotaeq  5064  iotabi  5065  fneq1  5179  fnun  5197  fnresdisj  5201  fnimadisj  5211  fnimaeq0  5212  sbcfng  5238  foeq1  5309  foco  5323  fveqeq2d  5395  fvelimab  5443  fvun1  5453  fvmptdv2  5476  fneqeql  5494  dffo3  5533  fvsng  5582  fconstfvm  5604  eufnfv  5614  f1veqaeq  5636  dff13f  5637  f1elima  5640  foeqcnvco  5657  f1eqcocnv  5658  acexmidlemab  5734  ovanraleqv  5764  eloprabga  5824  ovmpodv2  5870  ovi3  5873  ovelimab  5887  caovcang  5898  caovcan  5901  caovimo  5930  grprinvlem  5931  grpridd  5933  suppssfv  5944  suppssov1  5945  caofinvl  5970  op1stg  6014  op2ndg  6015  eqop  6041  reldm  6050  xporderlem  6094  tposfo2  6130  frec0g  6260  freccllem  6265  frecfcllem  6267  frecsuclem  6269  frecsuc  6270  nnm0r  6341  nnmord  6379  nnaordex  6389  nnawordex  6390  ereq1  6402  eqerlem  6426  mapsn  6550  endisj  6684  xpf1o  6704  mapxpen  6708  fidifsnen  6730  supelti  6855  updjudhcoinlf  6931  updjudhcoinrg  6932  updjud  6933  omp1eomlem  6945  difinfsnlem  6950  enomnilem  6976  finomni  6978  exmidomni  6980  fodjuomnilemres  6986  fodjuomni  6987  ismkvnex  6995  mkvprop  6998  fodjumkvlemres  6999  pm54.43  7012  exmidfodomrlemrALT  7023  addnidpig  7108  ltexpi  7109  dfplpq2  7126  dfmpq2  7127  recexnq  7162  recmulnqg  7163  ltexnqq  7180  halfnqq  7182  enq0tr  7206  nqnq0pi  7210  addnnnq0  7221  addlocpr  7308  ltexprlemru  7384  ltexpri  7385  lteupri  7389  prplnqu  7392  recexpr  7410  addsrpr  7517  mulsrpr  7518  00sr  7541  negexsr  7544  recexgt0sr  7545  srpospr  7555  prsrriota  7560  caucvgsrlemfv  7563  map2psrprg  7577  elrealeu  7601  axrnegex  7651  axprecex  7652  rereceu  7661  recriota  7662  nntopi  7666  axcaucvglemval  7669  axcaucvglemcau  7670  cnegexlem1  7901  cnegex  7904  cnegex2  7905  subval  7918  subadd  7929  subadd2  7930  subsub23  7931  addsubeq4  7941  subcan2  7951  negcon1  7978  subcan  7981  addrsub  8097  ltadd2  8145  ltordlem  8208  recexre  8303  recexap  8377  muleqadd  8392  receuap  8393  divvalap  8397  divmulap  8398  rec11ap  8433  zdiv  9093  uzin  9310  xaddval  9579  xnn0xadd0  9601  xnegdi  9602  xltadd1  9610  icc0r  9660  fznlem  9772  fseq1m1p1  9826  1fv  9867  fzon  9894  fvinim0ffz  9969  ioo0  9988  ico0  9990  ioc0  9991  flqbi  10014  divfl0  10020  modq0  10053  modqmuladdnn0  10092  addmodlteq  10122  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  seq3f1olemstep  10225  seq3f1olemp  10226  seq3id  10232  seq3z  10235  mulreap  10587  rennim  10725  resqrexlemex  10748  rsqrmo  10750  resqrtcl  10752  rersqrtthlem  10753  sqrtsq2  10766  isumss  11111  fsum00  11182  telfsumo  11186  pwm1geoserap1  11228  absefib  11386  efieq1re  11387  divides  11402  dvdsval2  11403  nndivides  11407  dvds0lem  11410  dvds1lem  11411  dvds2lem  11412  negdvdsb  11416  muldvds1  11425  muldvds2  11426  dvdscmulr  11429  dvdsmulcr  11430  dvdstr  11437  dvdsabseq  11452  divconjdvds  11454  odd2np1lem  11476  odd2np1  11477  even2n  11478  oddm1even  11479  2tp1odd  11488  opeo  11501  omeo  11502  m1exp1  11505  divalgb  11529  gcdaddm  11579  gcdabs1  11584  bezout  11606  gcdmultiple  11615  gcdmultiplez  11616  rplpwr  11622  rppwr  11623  alginv  11635  algcvga  11639  algfx  11640  eucalgval2  11641  coprmdvds  11680  qredeq  11684  qredeu  11685  divgcdcoprm0  11689  divgcdcoprmex  11690  cncongr1  11691  rpexp  11738  rpexp12i  11740  cncongrprm  11742  qnumdenbi  11776  phival  11795  phicl2  11796  dfphi2  11802  phiprmpw  11804  phimullem  11807  hashgcdlem  11809  ennnfonelemhf1o  11832  ntreq0  12207  ispsmet  12398  psmet0  12402  ismet  12419  isxmet  12420  xmeteq0  12434  metn0  12453  xmetres2  12454  xblss2ps  12479  xblss2  12480  xmseq0  12543  comet  12574  bdxmet  12576  cnmet  12605  ivthdec  12697  pwle2  13027  subctctexmid  13030  peano4nninf  13034  nninfalllemn  13036  nninfalllem1  13037  nninfsellemdc  13040  nninfsellemeq  13044  nninfsellemqall  13045  nninfsellemeqinf  13046  nninfomnilem  13048  nninfomni  13049  isomninnlem  13059  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator