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  3306  axpow3  4149  isocnv  5747  qextlt  10482  qextle  10483  rpnnen2  12452  odd2np1  12535  nrmmetd  18045  cvmlift2lem12  23203  wl-bibi2d  24277  oriso  24567  nn0prpw  25592  bicomdd  26058  compneOLD  26997  aibandbiaiffaiffb  27137  aibandbiaiaiffb  27138  notatnand  27139  aistia  27140  aisfina  27141  bothfbothsame  27143  aiffnbandciffatnotciffb  27147  axorbciffatcxorb  27148  aibnbna  27149  aisbnaxb  27154  abnotbtaxb  27159  abnotataxb  27160  3impexpbicomVD  27667  bnj926  27832
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