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

Theorem equcomi 1684
Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
equcomi  |-  ( x  =  y  ->  y  =  x )

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1681 . 2  |-  x  =  x
2 ax-8 1484 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
31, 2mpi 15 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  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:  ax6evr  1685  equcom  1686  equcoms  1688  ax10  1697  cbv2h  1728  cbv2w  1730  equvini  1738  equveli  1739  equsb2  1766  drex1  1778  sbcof2  1790  aev  1792  cbvexdh  1906  rext  4176  iotaval  5147  prodmodc  11479
  Copyright terms: Public domain W3C validator