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

Theorem eqeq1i 2148
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  =  C  <->  B  =  C )

Proof of Theorem eqeq1i
StepHypRef Expression
1 eqeq1i.1 . 2  |-  A  =  B
2 eqeq1 2147 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
31, 2ax-mp 5 1  |-  ( A  =  C  <->  B  =  C )
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 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  ssequn2  3252  dfss1  3283  disj  3414  disjr  3415  undisj1  3423  undisj2  3424  uneqdifeqim  3451  reusn  3600  rabsneu  3602  eusn  3603  iin0r  4099  opeqsn  4180  unisuc  4341  onsucelsucexmid  4451  sucprcreg  4470  onintexmid  4493  dmopab3  4758  dm0rn0  4762  ssdmres  4847  imadisj  4907  args  4914  intirr  4931  dminxp  4989  dfrel3  5002  fntpg  5185  fncnv  5195  f0rn0  5323  dff1o4  5381  dffv4g  5424  fvun2  5494  fnreseql  5536  riota1  5754  riota2df  5756  fnotovb  5820  ovid  5893  ov  5896  ovg  5915  f1od2  6138  frec0g  6300  diffitest  6787  ismkvnex  7035  prarloclem5  7330  renegcl  8045  elznn0  9091  hashunlem  10580  maxclpr  11024  ex-ceil  13102  nninfsellemqall  13379  nninfomni  13383
  Copyright terms: Public domain W3C validator