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  803  con2biddc  808  pm5.17dc  844  bigolden  897  nbbndc  1326  bilukdc  1328  falbitru  1349  3impexpbicom  1368  exists1  2039  eqcom  2085  abeq1  2192  necon2abiddc  2315  necon2bbiddc  2316  necon4bbiddc  2323  ssequn1  3152  axpow3  3971  isocnv  5502  bezoutlemle  10604