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

Theorem equcom 1683
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 1681 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1681 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 125 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> 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 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equcomd  1684  sbal1yz  1977  dveeq1  1995  eu1  2025  reu7  2882  reu8  2883  dfdif3  3190  iunid  3875  copsexg  4173  opelopabsbALT  4188  dtruex  4481  opeliunxp  4601  relop  4696  dmi  4761  opabresid  4879  intirr  4932  cnvi  4950  coi1  5061  brprcneu  5421  f1oiso  5734  qsid  6501  mapsnen  6712  suplocsrlem  7639  summodc  11183  bezoutlemle  11730  cnmptid  12487
  Copyright terms: Public domain W3C validator