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

Theorem eqeq2d 2093
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
eqeq2d (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))

Proof of Theorem eqeq2d
StepHypRef Expression
1 eqeq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeq2 2091 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2syl 14 1 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eqtrd  2114  eq2tri  2141  rspcedeq2vd  2711  sbceq1g  2927  euabsn  3470  absneu  3472  preq12bg  3573  cbvopab  3857  cbvopab1  3859  cbvopab2  3860  cbvopab1s  3861  cbvopab2v  3863  mpteq12f  3866  cbvmpt  3880  opth  4000  eqvinop  4006  moop2  4014  euotd  4017  eusvnf  4211  reusv3i  4217  nlimsucg  4317  nn0suc  4353  opelxp  4400  elvvv  4429  relop  4514  elrnmpt1s  4612  elrnmpt1  4613  elsnres  4675  elxp4  4838  elxp5  4839  relresfld  4877  iotajust  4896  iota1  4911  iota2df  4921  funopg  4964  funcnvuni  4999  fun11iun  5178  funcocnv2  5182  nfvres  5238  ssimaex  5266  fvmptg  5280  fvmptdf  5290  fvopab6  5296  foco2  5350  fmptco  5362  fsng  5368  elabrex  5429  abrexco  5430  f1veqaeq  5440  dff13f  5441  f1ocnvfv  5450  f1ocnvfvb  5451  fcofo  5455  fliftfun  5467  fliftval  5471  f1oiso2  5497  riota5f  5523  oprabid  5568  rspceov  5578  dfoprab2  5583  mpt2eq123dva  5597  mpt2eq3dva  5600  cbvoprab1  5607  cbvoprab2  5608  cbvoprab12  5609  cbvmpt2x  5613  mpt2mptx  5626  ovmpt2s  5655  ovmpt2df  5663  ovmpt2dv2  5665  ovi3  5668  ov6g  5669  fnrnov  5677  foov  5678  caovcang  5693  caovcan  5696  f1opw2  5737  opabex3d  5779  opabex3  5780  fo1st  5815  fo2nd  5816  elxp6  5827  op1steq  5836  dfoprab4f  5850  fmpt2x  5857  df1st2  5871  df2nd2  5872  xporderlem  5883  cnvoprab  5886  f1od2  5887  brtpos2  5900  dftpos4  5912  tposfn2  5915  recseq  5955  tfr1onlemaccex  5997  tfrcllemaccex  6010  frecabcl  6048  frecsuc  6056  nna0r  6122  eqerlem  6203  qseq2  6221  ecelqsg  6225  snec  6233  qsinxp  6248  ecoptocl  6259  eroveu  6263  th3qlem1  6274  th3qlem2  6275  th3q  6277  en1  6346  xpsnen  6365  xpassen  6374  xpf1o  6385  fidifsnen  6405  ac6sfi  6431  undiffi  6443  dfplpq2  6606  dfmpq2  6607  enqbreq2  6609  enq0sym  6684  enq0ref  6685  enq0tr  6686  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  mulnnnq0  6702  nqnq0a  6706  nqnq0m  6707  nq0a0  6709  prarloclemcalc  6754  genipv  6761  genpassl  6776  genpassu  6777  addcomprg  6830  mulcomprg  6832  distrlem1prl  6834  distrlem1pru  6835  distrlem5prl  6838  distrlem5pru  6839  1idprl  6842  1idpru  6843  recexprlem1ssl  6885  recexprlem1ssu  6886  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  elreal  7059  axcnre  7109  axcaucvglemval  7125  negeu  7366  subeq0  7401  apreap  7754  apreim  7770  divmulap3  7832  diveqap0  7837  diveqap1  7860  nn0ind-raph  8545  elq  8788  zq  8792  cnref1o  8814  iccf1o  9102  fzen  9138  fseq1m1p1  9188  fzm1  9193  modqmuladd  9448  modqmuladdnn0  9450  modfzo0difsn  9477  nn0ennn  9515  iseqid2  9564  ibcval5  9787  sizeen1  9823  shftlem  9842  shftfvalg  9844  shftfval  9847  negfi  10248  sumeq2d  10334  sumeq2  10335  moddvds  10349  dvdsnegb  10357  dvdsabseq  10392  dvdsmod  10407  odd2np1lem  10416  odd2np1  10417  opeo  10441  omeo  10442  divalglemnn  10462  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  bezoutlemnewy  10529  bezoutlema  10532  bezoutlemb  10533  bezoutlemex  10534  bezoutlemaz  10536  bezoutlembz  10537  eucalglt  10583  qredeq  10622  qredeu  10623  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  evenennn  10704  bj-nn0suc0  10903  bj-inf2vnlem1  10923  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator