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

Theorem bicom 192
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 191 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
2 bicom1 191 . 2  |-  ( ( ps  <->  ph )  ->  ( ph 
<->  ps ) )
31, 2impbii 181 1  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bicomd  193  bibi1i  306  bibi1d  311  con2bi  319  ibibr  333  bibif  336  nbbn  348  pm5.17  859  biluk  900  bigolden  902  xorcom  1313  falbitru  1358  3impexpbicom  1373  mtp-xorOLD  1543  exists1  2347  eqcom  2410  abeq1  2514  ssequn1  3481  axpow3  4344  isocnv  6013  qextlt  10749  qextle  10750  rpnnen2  12784  odd2np1  12867  nrmmetd  18579  cusgrauvtxb  21462  cvmlift2lem12  24958  wl-bibi2d  26134  nn0prpw  26220  bicomdd  26583  3impexpbicomVD  28682  bnj926  28848
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 178
  Copyright terms: Public domain W3C validator