Theorem bicom 128

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

Syntax hints:   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicomd  129  bibi1i  217  bibi1d  222  ibibr  235  bibif  614  con2bidc  769  con2biddc  774  pm5.17dc  810  bigolden  862  nbbndc  1285  bilukdc  1287  falbitru  1308  3impexpbicom  1327  exists1  1996  eqcom  2042  abeq1  2147  necon2abiddc  2271  necon2bbiddc  2272  necon4bbiddc  2279  ssequn1  3113  axpow3  3930  isocnv  5451