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  2233  eqcom  2286  abeq1  2390  ssequn1  3346  axpow3  4190  isocnv  5788  qextlt  10524  qextle  10525  rpnnen2  12498  odd2np1  12581  nrmmetd  18091  cvmlift2lem12  23249  wl-bibi2d  24323  oriso  24613  nn0prpw  25638  bicomdd  26104  compneOLD  27042  aibandbiaiffaiffb  27241  aibandbiaiaiffb  27242  notatnand  27243  aistia  27244  aisfina  27245  bothfbothsame  27247  aiffnbandciffatnotciffb  27251  axorbciffatcxorb  27252  aibnbna  27253  aisbnaxb  27258  abnotbtaxb  27263  abnotataxb  27264  3impexpbicomVD  27901  bnj926  28066
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