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

Theorem equequ1 1688
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 1482 . 2  |-  ( x  =  y  ->  (
x  =  z  -> 
y  =  z ) )
2 equtr 1685 . 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equveli  1732  drsb1  1771  equsb3lem  1923  euequ1  2094  axext3  2122  reu6  2873  reu7  2879  disjiun  3924  cbviota  5093  dff13f  5671  poxp  6129  dcdifsnid  6400  supmoti  6880  isoti  6894  fsum2dlemstep  11210  ennnfonelemr  11942  ctinf  11949
  Copyright terms: Public domain W3C validator