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

Theorem equequ2 1713
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 1710 . 2  |-  ( x  =  y  ->  (
z  =  x  -> 
z  =  y ) )
2 equtrr 1710 . . 3  |-  ( y  =  x  ->  (
z  =  y  -> 
z  =  x ) )
32equcoms 1708 . 2  |-  ( x  =  y  ->  (
z  =  y  -> 
z  =  x ) )
41, 3impbid 129 1  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ax11v2  1820  ax11v  1827  ax11ev  1828  equs5or  1830  eujust  2028  euf  2031  mo23  2067  eleq1w  2238  cbvabw  2300  csbcow  3070  disjiun  4000  iotaval  5191  dffun4f  5234  dff13f  5773  supmoti  6994  isoti  7008  nninfwlpoim  7178  exmidontriim  7226  netap  7255  ennnfonelemr  12426  ctinf  12433  infpn2  12459  lgseisenlem2  14490
  Copyright terms: Public domain W3C validator