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

Theorem eqeq1d 2048
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 2046 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2syl 14 1 (𝜑 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  sbceq2g  2872  csbhypf  2885  csbiebt  2886  csbiebg  2889  disjssun  3285  sneqrg  3533  preq12b  3541  preq12bg  3544  iin0r  3922  opthg  3975  opeqsn  3989  unisucg  4151  opthreg  4280  tfisi  4310  dmsnopg  4792  relcoi1  4849  iotaeq  4875  iotabi  4876  fneq1  4987  fnun  5005  fnresdisj  5009  fnimadisj  5019  fnimaeq0  5020  sbcfng  5044  foeq1  5102  foco  5116  fvelimab  5229  fvun1  5239  fvmptdv2  5260  fneqeql  5275  dffo3  5314  fvsng  5359  fconstfvm  5379  eufnfv  5389  f1veqaeq  5408  dff13f  5409  f1elima  5412  foeqcnvco  5430  f1eqcocnv  5431  acexmidlemab  5506  eloprabga  5591  ovmpt2dv2  5634  ovi3  5637  ovelimab  5651  caovcang  5662  caovcan  5665  caovimo  5694  grprinvlem  5695  grpridd  5697  suppssfv  5708  suppssov1  5709  caofinvl  5733  op1stg  5777  op2ndg  5778  eqop  5803  reldm  5812  xporderlem  5852  tposfo2  5882  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnm0r  6058  nnmord  6090  nnaordex  6100  nnawordex  6101  ereq1  6113  eqerlem  6137  endisj  6298  fidifsnen  6331  addnidpig  6432  ltexpi  6433  dfplpq2  6450  dfmpq2  6451  recexnq  6486  recmulnqg  6487  ltexnqq  6504  halfnqq  6506  enq0tr  6530  nqnq0pi  6534  addnnnq0  6545  addlocpr  6632  ltexprlemru  6708  ltexpri  6709  lteupri  6713  prplnqu  6716  recexpr  6734  addsrpr  6828  mulsrpr  6829  00sr  6852  negexsr  6855  recexgt0sr  6856  srpospr  6865  prsrriota  6870  caucvgsrlemfv  6873  elrealeu  6904  axrnegex  6951  axprecex  6952  rereceu  6961  recriota  6962  nntopi  6966  axcaucvglemval  6969  axcaucvglemcau  6970  cnegexlem1  7184  cnegex  7187  cnegex2  7188  subval  7201  subadd  7212  subadd2  7213  subsub23  7214  addsubeq4  7224  subcan2  7234  negcon1  7261  subcan  7264  ltadd2  7414  recexre  7567  recexap  7632  muleqadd  7647  receuap  7648  divvalap  7651  divmulap  7652  rec11ap  7684  zdiv  8326  uzin  8503  icc0r  8793  fznlem  8903  fseq1m1p1  8955  1fv  8994  fzon  9020  fvinim0ffz  9094  flqbi  9130  divfl0  9136  frecuzrdgfn  9172  iseqid3s  9220  iseqid  9221  mulreap  9438  rennim  9574  resqrexlemex  9597  rsqrmo  9599  resqrtcl  9601  rersqrtthlem  9602  sqrtsq2  9615  ialginv  9860  ialgcvga  9864  ialgfx  9865
  Copyright terms: Public domain W3C validator