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

Theorem eqeq1i 2162
 Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eqeq1i (𝐴 = 𝐶𝐵 = 𝐶)

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2 𝐴 = 𝐵
2 eqeq1 2161 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1332 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 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-cleq 2147 This theorem is referenced by:  ssequn2  3276  dfss1  3307  disj  3438  disjr  3439  undisj1  3447  undisj2  3448  uneqdifeqim  3475  reusn  3626  rabsneu  3628  eusn  3629  iin0r  4125  opeqsn  4207  unisuc  4368  onsucelsucexmid  4483  sucprcreg  4502  onintexmid  4526  dmopab3  4792  dm0rn0  4796  ssdmres  4881  imadisj  4941  args  4948  intirr  4965  dminxp  5023  dfrel3  5036  fntpg  5219  fncnv  5229  f0rn0  5357  dff1o4  5415  dffv4g  5458  fvun2  5528  fnreseql  5570  riota1  5788  riota2df  5790  fnotovb  5854  ovid  5927  ov  5930  ovg  5949  f1od2  6172  frec0g  6334  diffitest  6821  ismkvnex  7077  prarloclem5  7399  renegcl  8115  elznn0  9161  hashunlem  10655  maxclpr  11099  ex-ceil  13248  nninfsellemqall  13536  nninfomni  13540  iswomni0  13571
 Copyright terms: Public domain W3C validator