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

Theorem equcom 1717
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 1715 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1715 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 126 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  equcomd  1718  sbal1yz  2013  dveeq1  2031  eu1  2063  reu7  2947  reu8  2948  dfdif3  3260  iunid  3957  copsexg  4262  opelopabsbALT  4277  dtruex  4576  opeliunxp  4699  relop  4795  dmi  4860  opabresid  4978  intirr  5033  cnvi  5051  coi1  5162  brprcneu  5527  f1oiso  5848  qsid  6626  mapsnen  6837  suplocsrlem  7837  summodc  11423  bezoutlemle  12041  cnmptid  14238
  Copyright terms: Public domain W3C validator