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

Theorem bicom 138
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 129 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 129 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 124 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
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
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bicomd  139  bibi1i  226  bibi1d  231  ibibr  244  bibif  647  con2bidc  803  con2biddc  808  pm5.17dc  844  bigolden  897  nbbndc  1326  bilukdc  1328  falbitru  1349  3impexpbicom  1368  exists1  2039  eqcom  2085  abeq1  2192  necon2abiddc  2315  necon2bbiddc  2316  necon4bbiddc  2323  ssequn1  3152  axpow3  3971  isocnv  5502  bezoutlemle  10604
  Copyright terms: Public domain W3C validator