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

Theorem equequ1 1646
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 1441 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1643 . 2  |-  ( x  =  y  ->  (
y  =  z  ->  x  =  z )
)
31, 2impbid 128 1  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1384  ax-ie2 1429  ax-8 1441  ax-17 1465  ax-i9 1469
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equveli  1690  drsb1  1728  equsb3lem  1873  euequ1  2044  axext3  2072  reu6  2807  reu7  2813  disjiun  3848  cbviota  5000  dff13f  5565  poxp  6013  dcdifsnid  6279  supmoti  6744  isoti  6758  fsum2dlemstep  10891
  Copyright terms: Public domain W3C validator