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

Theorem bicom 139
Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 11-Nov-2012.)
Assertion
Ref Expression
bicom  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )

Proof of Theorem bicom
StepHypRef Expression
1 bicom1 130 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 130 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 125 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bicomd  140  bibi1i  227  bibi1d  232  ibibr  245  bibif  672  con2bidc  845  con2biddc  850  pm5.17dc  874  bigolden  924  nbbndc  1357  bilukdc  1359  falbitru  1380  3impexpbicom  1399  exists1  2073  eqcom  2119  abeq1  2227  necon2abiddc  2351  necon2bbiddc  2352  necon4bbiddc  2359  ssequn1  3216  axpow3  4071  isocnv  5680  suplocsrlem  7584  uzennn  10177  bezoutlemle  11623
  Copyright terms: Public domain W3C validator