Theorem bicom 212

Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)

Assertion

Ref	Expression
bicom	|- ( ( ph <-> ps ) <-> ( ps <-> ph ) )

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		bicom1 211	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
2		bicom1 211	. 2 |- ( ( ps <-> ph ) -> ( ph <-> ps ) )
3	1, 2	impbii 199	1 |- ( ( ph <-> ps ) <-> ( ps <-> ph ) )

Syntax hints:   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  bicomd  213  bibi1i  328  bibi1d  333  con2bi  343  ibibr  358  bibif  361  nbbn  373  pm5.17  932  biluk  974  bigolden  976  xorcom  1467  trubifal  1522  exists1  2561  abeq1  2733  ssequn1  3783  axpow3  4846  isocnv  6580  qextlt  12034  qextle  12035  rpnnen2lem12  14954  odd2np1  15065  sumodd  15111  nrmmetd  22379  lgsqrmodndvds  25078  cvmlift2lem12  31296  nn0prpw  32318  bj-abeq1  32774  tsbi4  33943  bicomdd  34138  ifpbicor  37820  rp-fakeoranass  37859  or3or  38319  3impexpbicom  38685  3impexpbicomVD  39092  limsupreuz  39969  nabctnabc  41098