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

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

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq2 2094 . 2  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( C  =  A  <-> 
C  =  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = 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:  eqtrd  2117  eq2tri  2144  rspcedeq2vd  2723  sbceq1g  2940  euabsn  3495  absneu  3497  preq12bg  3600  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab2v  3890  mpteq12f  3893  cbvmpt  3907  opth  4037  eqvinop  4043  moop2  4051  euotd  4054  eusvnf  4248  reusv3i  4254  nlimsucg  4354  nn0suc  4391  opelxp  4439  elvvv  4468  relop  4553  elrnmpt1s  4652  elrnmpt1  4653  elsnres  4715  elxp4  4881  elxp5  4882  relresfld  4923  iotajust  4942  iota1  4957  iota2df  4967  funopg  5010  funcnvuni  5045  fun11iun  5231  funcocnv2  5235  nfvres  5294  ssimaex  5322  fvmptg  5337  fvmptdf  5347  fvopab6  5353  fmptco  5421  fsng  5427  foco2  5488  elabrex  5492  abrexco  5493  f1veqaeq  5503  dff13f  5504  f1ocnvfv  5513  f1ocnvfvb  5514  fcofo  5518  fliftfun  5530  fliftval  5534  f1oiso2  5561  riota5f  5587  oprabid  5632  rspceov  5642  dfoprab2  5647  mpt2eq123dva  5661  mpt2eq3dva  5664  cbvoprab1  5671  cbvoprab2  5672  cbvoprab12  5673  cbvmpt2x  5677  mpt2mptx  5690  ovmpt2s  5719  ovmpt2df  5727  ovmpt2dv2  5729  ovi3  5732  ov6g  5733  fnrnov  5741  foov  5742  caovcang  5757  caovcan  5760  f1opw2  5801  opabex3d  5843  opabex3  5844  fo1st  5879  fo2nd  5880  elxp6  5891  op1steq  5900  dfoprab4f  5914  fmpt2x  5921  df1st2  5935  df2nd2  5936  xporderlem  5947  cnvoprab  5950  f1od2  5951  brtpos2  5964  dftpos4  5976  tposfn2  5979  recseq  6019  tfr1onlemaccex  6061  tfrcllemaccex  6074  frecabcl  6112  frecsuc  6120  nna0r  6187  eqerlem  6269  qseq2  6287  ecelqsg  6291  snec  6299  qsinxp  6314  ecoptocl  6325  eroveu  6329  th3qlem1  6340  th3qlem2  6341  th3q  6343  mapsncnv  6398  en1  6462  mapsnen  6474  xpsnen  6483  xpassen  6492  xpf1o  6506  mapen  6508  mapxpen  6510  fidifsnen  6532  ac6sfi  6560  undifdc  6580  djuf1olem  6682  djur  6694  updjud  6710  fodjuomnilemdc  6736  fodjuomnilem0  6739  fodjuomni  6741  exmidfodomrlemeldju  6762  exmidfodomrlemreseldju  6763  dfplpq2  6850  dfmpq2  6851  enqbreq2  6853  enq0sym  6928  enq0ref  6929  enq0tr  6930  addnq0mo  6943  mulnq0mo  6944  addnnnq0  6945  mulnnnq0  6946  nqnq0a  6950  nqnq0m  6951  nq0a0  6953  prarloclemcalc  6998  genipv  7005  genpassl  7020  genpassu  7021  addcomprg  7074  mulcomprg  7076  distrlem1prl  7078  distrlem1pru  7079  distrlem5prl  7082  distrlem5pru  7083  1idprl  7086  1idpru  7087  recexprlem1ssl  7129  recexprlem1ssu  7130  addsrmo  7226  mulsrmo  7227  addsrpr  7228  mulsrpr  7229  elreal  7303  axcnre  7353  axcaucvglemval  7369  negeu  7610  subeq0  7645  apreap  7998  apreim  8014  divmulap3  8076  diveqap0  8081  diveqap1  8104  nn0ind-raph  8789  elq  9032  zq  9036  cnref1o  9058  iccf1o  9346  fzen  9382  fseq1m1p1  9432  fzm1  9437  modqmuladd  9694  modqmuladdnn0  9696  modfzo0difsn  9723  nn0ennn  9761  iseqid2  9836  ibcval5  10060  fihashen1  10096  shftlem  10139  shftfvalg  10141  shftfval  10144  negfi  10545  sumeq2  10631  isummo  10655  fisum  10658  moddvds  10672  dvdsnegb  10680  dvdsabseq  10715  dvdsmod  10730  odd2np1lem  10739  odd2np1  10740  opeo  10764  omeo  10765  divalglemnn  10785  divalglemeunn  10788  divalglemex  10789  divalglemeuneg  10790  bezoutlemnewy  10852  bezoutlema  10855  bezoutlemb  10856  bezoutlemex  10857  bezoutlemaz  10859  bezoutlembz  10860  eucalglt  10906  qredeq  10945  qredeu  10946  divgcdcoprm0  10950  divgcdcoprmex  10951  cncongr1  10952  cncongr2  10953  qnumdenbi  11037  hashgcdlem  11070  evenennn  11073  bj-nn0suc0  11275  bj-inf2vnlem1  11295  bj-nn0sucALT  11303
  Copyright terms: Public domain W3C validator