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

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

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2 A = B
2 eqeq1 2028 . 2 (A = B → (A = 𝐶B = 𝐶))
31, 2ax-mp 7 1 (A = 𝐶B = 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  ssequn2  3093  dfss1  3118  disj  3245  disjr  3246  undisj1  3256  undisj2  3257  uneqdifeqim  3285  reusn  3415  rabsneu  3417  eusn  3418  iin0r  3896  opeqsn  3963  unisuc  4099  onsucelsucexmid  4199  sucprcreg  4211  dmopab3  4475  dm0rn0  4479  ssdmres  4560  imadisj  4614  args  4621  intirr  4638  dminxp  4692  dfrel3  4705  fntpg  4881  fncnv  4891  dff1o4  5059  dffv4g  5100  fvun2  5165  fnreseql  5202  riota1  5410  riota2df  5412  fnotovb  5471  ovid  5540  ov  5543  ovg  5562  prarloclem5  6354  renegcl  6858
  Copyright terms: Public domain W3C validator