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

Theorem equequ1 1723
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
equequ1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )

Proof of Theorem equequ1
StepHypRef Expression
1 ax-8 1515 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1720 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 129 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  equveli  1770  drsb1  1810  equsb3lem  1962  euequ1  2133  axext3  2172  cbvreuvw  2724  reu6  2941  reu7  2947  disjiun  4016  cbviota  5204  dff13f  5795  poxp  6261  dcdifsnid  6533  supmoti  7026  isoti  7040  nninfwlpoim  7211  exmidontriimlem3  7257  exmidontriim  7259  netap  7288  fsum2dlemstep  11483  ennnfonelemr  12485  ctinf  12492  reap0  15294
  Copyright terms: Public domain W3C validator