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

Theorem bicom 193
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 192 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 192 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 182 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  bicomd  194  bibi1i  307  bibi1d  312  con2bi  320  ibibr  334  bibif  337  nbbn  349  pm5.17  863  biluk  904  bigolden  906  xorcom  1303  falbitru  1348  3impexpbicom  1363  mtp-xor  1530  exists1  2205  eqcom  2258  abeq1  2362  ssequn1  3287  axpow3  4129  isocnv  5726  qextlt  10461  qextle  10462  rpnnen2  12431  odd2np1  12514  nrmmetd  18024  cvmlift2lem12  23182  wl-bibi2d  24256  oriso  24546  nn0prpw  25571  bicomdd  26037  compneOLD  26976  aibandbiaiffaiffb  27116  aibandbiaiaiffb  27117  notatnand  27118  aistia  27119  aisfina  27120  bothfbothsame  27122  aiffnbandciffatnotciffb  27126  axorbciffatcxorb  27127  aibnbna  27128  aisbnaxb  27133  abnotbtaxb  27138  abnotataxb  27139  3impexpbicomVD  27646  bnj926  27811
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator