Theorem bicom 138

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 129	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
2		bicom1 129	. 2 |- ( ( ps <-> ph ) -> ( ph <-> ps ) )
3	1, 2	impbii 124	1 |- ( ( ph <-> ps ) <-> ( ps <-> ph ) )

Syntax hints:   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicomd  139  bibi1i  226  bibi1d  231  ibibr  244  bibif  647  con2bidc  805  con2biddc  810  pm5.17dc  846  bigolden  899  nbbndc  1328  bilukdc  1330  falbitru  1351  3impexpbicom  1370  exists1  2041  eqcom  2087  abeq1  2194  necon2abiddc  2317  necon2bbiddc  2318  necon4bbiddc  2325  ssequn1  3159  axpow3  3989  isocnv  5553  bezoutlemle  10922