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

Theorem eqeq1d 2091
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 2089 . 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 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  rspcedeq1vd  2717  sbceq2g  2937  csbhypf  2950  csbiebt  2951  csbiebg  2954  disjssun  3323  sneqrg  3574  preq12b  3582  preq12bg  3585  iin0r  3963  opthg  4021  opeqsn  4035  unisucg  4197  opthreg  4327  tfisi  4356  dmsnopg  4842  relcoi1  4899  iotaeq  4925  iotabi  4926  fneq1  5038  fnun  5056  fnresdisj  5060  fnimadisj  5070  fnimaeq0  5071  sbcfng  5095  foeq1  5154  foco  5168  fvelimab  5282  fvun1  5292  fvmptdv2  5313  fneqeql  5328  dffo3  5367  fvsng  5412  fconstfvm  5432  eufnfv  5442  f1veqaeq  5461  dff13f  5462  f1elima  5465  foeqcnvco  5482  f1eqcocnv  5483  acexmidlemab  5558  eloprabga  5643  ovmpt2dv2  5686  ovi3  5689  ovelimab  5703  caovcang  5714  caovcan  5717  caovimo  5746  grprinvlem  5747  grpridd  5749  suppssfv  5760  suppssov1  5761  caofinvl  5785  op1stg  5829  op2ndg  5830  eqop  5855  reldm  5864  xporderlem  5904  tposfo2  5937  frec0g  6067  freccllem  6072  frecfcllem  6074  frecsuclem  6076  frecsuc  6077  nnm0r  6144  nnmord  6178  nnaordex  6188  nnawordex  6189  ereq1  6201  eqerlem  6225  endisj  6390  xpf1o  6407  fidifsnen  6427  supelti  6510  updjudhcoinlf  6574  updjudhcoinrg  6575  updjud  6576  pm54.43  6588  addnidpig  6658  ltexpi  6659  dfplpq2  6676  dfmpq2  6677  recexnq  6712  recmulnqg  6713  ltexnqq  6730  halfnqq  6732  enq0tr  6756  nqnq0pi  6760  addnnnq0  6771  addlocpr  6858  ltexprlemru  6934  ltexpri  6935  lteupri  6939  prplnqu  6942  recexpr  6960  addsrpr  7054  mulsrpr  7055  00sr  7078  negexsr  7081  recexgt0sr  7082  srpospr  7091  prsrriota  7096  caucvgsrlemfv  7099  elrealeu  7130  axrnegex  7177  axprecex  7178  rereceu  7187  recriota  7188  nntopi  7192  axcaucvglemval  7195  axcaucvglemcau  7196  cnegexlem1  7420  cnegex  7423  cnegex2  7424  subval  7437  subadd  7448  subadd2  7449  subsub23  7450  addsubeq4  7460  subcan2  7470  negcon1  7497  subcan  7500  addrsub  7612  ltadd2  7660  recexre  7815  recexap  7880  muleqadd  7895  receuap  7896  divvalap  7899  divmulap  7900  rec11ap  7935  zdiv  8586  uzin  8802  icc0r  9095  fznlem  9206  fseq1m1p1  9258  1fv  9296  fzon  9322  fvinim0ffz  9397  ioo0  9416  ico0  9418  ioc0  9419  flqbi  9442  divfl0  9448  modq0  9481  modqmuladdnn0  9520  addmodlteq  9550  frecuzrdgtcl  9564  frecuzrdgfunlem  9571  iseqid3s  9632  iseqid  9633  iseqid2  9634  iseqz  9636  mulreap  9970  rennim  10107  resqrexlemex  10130  rsqrmo  10132  resqrtcl  10134  rersqrtthlem  10135  sqrtsq2  10148  fisumcvg  10419  divides  10423  dvdsval2  10424  nndivides  10428  dvds0lem  10431  dvds1lem  10432  dvds2lem  10433  negdvdsb  10437  muldvds1  10446  muldvds2  10447  dvdscmulr  10450  dvdsmulcr  10451  dvdstr  10458  dvdsabseq  10473  divconjdvds  10475  odd2np1lem  10497  odd2np1  10498  even2n  10499  oddm1even  10500  2tp1odd  10509  opeo  10522  omeo  10523  m1exp1  10526  divalgb  10550  gcdaddm  10600  gcdabs1  10605  bezout  10625  gcdmultiple  10634  gcdmultiplez  10635  rplpwr  10641  rppwr  10642  ialginv  10654  ialgcvga  10658  ialgfx  10659  eucalgval2  10660  coprmdvds  10699  qredeq  10703  qredeu  10704  divgcdcoprm0  10708  divgcdcoprmex  10709  cncongr1  10710  rpexp  10757  rpexp12i  10759  cncongrprm  10761  qnumdenbi  10795  phival  10814  phicl2  10815  dfphi2  10821  phiprmpw  10823  phimullem  10826  hashgcdlem  10828
  Copyright terms: Public domain W3C validator