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

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

Proof of Theorem eqeq1d
StepHypRef Expression
1 eqeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eqeq1 2146 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2syl 14 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  rspcedeq1vd  2798  sbceq2g  3024  csbhypf  3038  csbiebt  3039  csbiebg  3042  dfss4st  3309  disjssun  3426  sneqrg  3689  preq12b  3697  preq12bg  3700  disji2  3922  iin0r  4093  opthg  4160  opeqsn  4174  unisucg  4336  opthreg  4471  tfisi  4501  dmsnopg  5010  relcoi1  5070  iotaeq  5096  iotabi  5097  fneq1  5211  fnun  5229  fnresdisj  5233  fnimadisj  5243  fnimaeq0  5244  sbcfng  5270  foeq1  5341  foco  5355  fveqeq2d  5429  fvelimab  5477  fvun1  5487  fvmptdv2  5510  fneqeql  5528  dffo3  5567  fvsng  5616  fconstfvm  5638  eufnfv  5648  f1veqaeq  5670  dff13f  5671  f1elima  5674  foeqcnvco  5691  f1eqcocnv  5692  acexmidlemab  5768  ovanraleqv  5798  eloprabga  5858  ovmpodv2  5904  ovi3  5907  ovelimab  5921  caovcang  5932  caovcan  5935  caovimo  5964  grprinvlem  5965  grpridd  5967  suppssfv  5978  suppssov1  5979  caofinvl  6004  op1stg  6048  op2ndg  6049  eqop  6075  reldm  6084  xporderlem  6128  tposfo2  6164  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnm0r  6375  nnmord  6413  nnaordex  6423  nnawordex  6424  ereq1  6436  eqerlem  6460  mapsn  6584  endisj  6718  xpf1o  6738  mapxpen  6742  fidifsnen  6764  supelti  6889  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  omp1eomlem  6979  difinfsnlem  6984  enomnilem  7010  finomni  7012  exmidomni  7014  fodjuomnilemres  7020  fodjuomni  7021  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  pm54.43  7046  exmidfodomrlemrALT  7059  cc2lem  7081  addnidpig  7151  ltexpi  7152  dfplpq2  7169  dfmpq2  7170  recexnq  7205  recmulnqg  7206  ltexnqq  7223  halfnqq  7225  enq0tr  7249  nqnq0pi  7253  addnnnq0  7264  addlocpr  7351  ltexprlemru  7427  ltexpri  7428  lteupri  7432  prplnqu  7435  recexpr  7453  addsrpr  7560  mulsrpr  7561  00sr  7584  negexsr  7587  recexgt0sr  7588  srpospr  7598  prsrriota  7603  caucvgsrlemfv  7606  map2psrprg  7620  elrealeu  7644  axrnegex  7694  axprecex  7695  rereceu  7704  recriota  7705  nntopi  7709  axcaucvglemval  7712  axcaucvglemcau  7713  cnegexlem1  7944  cnegex  7947  cnegex2  7948  subval  7961  subadd  7972  subadd2  7973  subsub23  7974  addsubeq4  7984  subcan2  7994  negcon1  8021  subcan  8024  addrsub  8140  ltadd2  8188  ltordlem  8251  recexre  8347  recexap  8421  muleqadd  8436  receuap  8437  divvalap  8441  divmulap  8442  rec11ap  8477  zdiv  9146  uzin  9365  xaddval  9635  xnn0xadd0  9657  xnegdi  9658  xltadd1  9666  icc0r  9716  fznlem  9828  fseq1m1p1  9882  1fv  9923  fzon  9950  fvinim0ffz  10025  ioo0  10044  ico0  10046  ioc0  10047  flqbi  10070  divfl0  10076  modq0  10109  modqmuladdnn0  10148  addmodlteq  10178  frecuzrdgtcl  10192  frecuzrdgfunlem  10199  seq3f1olemstep  10281  seq3f1olemp  10282  seq3id  10288  seq3z  10291  mulreap  10643  rennim  10781  resqrexlemex  10804  rsqrmo  10806  resqrtcl  10808  rersqrtthlem  10809  sqrtsq2  10822  isumss  11167  fsum00  11238  telfsumo  11242  pwm1geoserap1  11284  absefib  11484  efieq1re  11485  divides  11502  dvdsval2  11503  nndivides  11507  dvds0lem  11510  dvds1lem  11511  dvds2lem  11512  negdvdsb  11516  muldvds1  11525  muldvds2  11526  dvdscmulr  11529  dvdsmulcr  11530  dvdstr  11537  dvdsabseq  11552  divconjdvds  11554  odd2np1lem  11576  odd2np1  11577  even2n  11578  oddm1even  11579  2tp1odd  11588  opeo  11601  omeo  11602  m1exp1  11605  divalgb  11629  gcdaddm  11679  gcdabs1  11684  bezout  11706  gcdmultiple  11715  gcdmultiplez  11716  rplpwr  11722  rppwr  11723  alginv  11735  algcvga  11739  algfx  11740  eucalgval2  11741  coprmdvds  11780  qredeq  11784  qredeu  11785  divgcdcoprm0  11789  divgcdcoprmex  11790  cncongr1  11791  rpexp  11838  rpexp12i  11840  cncongrprm  11842  qnumdenbi  11877  phival  11896  phicl2  11897  dfphi2  11903  phiprmpw  11905  phimullem  11908  hashgcdlem  11910  ennnfonelemhf1o  11933  ntreq0  12311  ispsmet  12502  psmet0  12506  ismet  12523  isxmet  12524  xmeteq0  12538  metn0  12557  xmetres2  12558  xblss2ps  12583  xblss2  12584  xmseq0  12647  comet  12678  bdxmet  12680  cnmet  12709  ivthdec  12801  ioocosf1o  12945  pwle2  13207  subctctexmid  13210  peano4nninf  13214  nninfalllemn  13216  nninfalllem1  13217  nninfsellemdc  13220  nninfsellemeq  13224  nninfsellemqall  13225  nninfsellemeqinf  13226  nninfomnilem  13228  nninfomni  13229  isomninnlem  13239  trilpolemlt1  13248
  Copyright terms: Public domain W3C validator