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  613  con2bidc  768  con2biddc  773  pm5.17dc  809  bigolden  861  nbbndc  1282  bilukdc  1284  falbitru  1305  3impexpbicom  1324  exists1  1993  eqcom  2039  abeq1  2144  necon2abiddc  2265  necon2bbiddc  2266  necon4bbiddc  2273  ssequn1  3107  axpow3  3921  isocnv  5394