Theorem bicom 139

Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 11-Nov-2012.)

Assertion

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

Proof of Theorem bicom

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

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicomd  140  bibi1i  227  bibi1d  232  ibibr  245  bibif  655  con2bidc  813  con2biddc  818  pm5.17dc  854  bigolden  907  nbbndc  1340  bilukdc  1342  falbitru  1363  3impexpbicom  1382  exists1  2056  eqcom  2102  abeq1  2209  necon2abiddc  2333  necon2bbiddc  2334  necon4bbiddc  2341  ssequn1  3193  axpow3  4041  isocnv  5644  uzennn  10050  bezoutlemle  11489