MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicom Unicode version

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

Proof of Theorem bicom
StepHypRef Expression
1 bicom1 190 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 190 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 180 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bicomd  192  bibi1i  305  bibi1d  310  con2bi  318  ibibr  332  bibif  335  nbbn  347  pm5.17  858  biluk  899  bigolden  901  xorcom  1298  falbitru  1342  3impexpbicom  1357  mtp-xor  1525  exists1  2232  eqcom  2285  abeq1  2389  ssequn1  3345  axpow3  4191  isocnv  5827  qextlt  10530  qextle  10531  rpnnen2  12504  odd2np1  12587  nrmmetd  18097  bisimpd  23120  iuninc  23158  cvmlift2lem12  23845  wl-bibi2d  24916  oriso  25214  nn0prpw  26239  bicomdd  26705  compneOLD  27643  aibandbiaiffaiffb  27862  aibandbiaiaiffb  27863  notatnand  27864  aistia  27865  aisfina  27866  bothfbothsame  27868  aiffnbandciffatnotciffb  27872  axorbciffatcxorb  27873  aibnbna  27874  aisbnaxb  27879  abnotbtaxb  27884  abnotataxb  27885  3impexpbicomVD  28633  bnj926  28799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator