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

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

Proof of Theorem equequ2
StepHypRef Expression
1 equtrr 1703 . 2  |-  ( x  =  y  ->  (
z  =  x  -> 
z  =  y ) )
2 equtrr 1703 . . 3  |-  ( y  =  x  ->  (
z  =  y  -> 
z  =  x ) )
32equcoms 1701 . 2  |-  ( x  =  y  ->  (
z  =  y  -> 
z  =  x ) )
41, 3impbid 128 1  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
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 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1813  ax11v  1820  ax11ev  1821  equs5or  1823  eujust  2021  euf  2024  mo23  2060  eleq1w  2231  cbvabw  2293  csbcow  3060  disjiun  3984  iotaval  5171  dffun4f  5214  dff13f  5749  supmoti  6970  isoti  6984  nninfwlpoim  7154  exmidontriim  7202  ennnfonelemr  12378  ctinf  12385  infpn2  12411
  Copyright terms: Public domain W3C validator