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

Theorem equequ2 1693
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 1690 . 2  |-  ( x  =  y  ->  (
z  =  x  -> 
z  =  y ) )
2 equtrr 1690 . . 3  |-  ( y  =  x  ->  (
z  =  y  -> 
z  =  x ) )
32equcoms 1688 . 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 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1800  ax11v  1807  ax11ev  1808  equs5or  1810  eujust  2008  euf  2011  mo23  2047  eleq1w  2218  cbvabw  2280  csbcow  3042  disjiun  3962  iotaval  5149  dffun4f  5189  dff13f  5723  supmoti  6940  isoti  6954  exmidontriim  7163  ennnfonelemr  12248  ctinf  12255
  Copyright terms: Public domain W3C validator