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

Theorem equcom 1635
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom  |-  ( x  =  y  <->  y  =  x )

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1633 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1633 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 124 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sbal1yz  1920  dveeq1  1938  eu1  1968  reu7  2796  reu8  2797  dfdif3  3092  iunid  3753  copsexg  4027  opelopabsbALT  4042  dtruex  4330  opeliunxp  4441  relop  4534  dmi  4598  opabresid  4709  intirr  4761  cnvi  4778  coi1  4886  brprcneu  5222  f1oiso  5516  qsid  6258  bezoutlemle  10604
  Copyright terms: Public domain W3C validator