Theorem bicomi 130

Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 16-Sep-2013.)

Hypothesis

Ref	Expression
bicomi.1	|- ( ph <-> ps )

Assertion

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

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 |- ( ph <-> ps )
2		bicom1 129	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
3	1, 2	ax-mp 7	1 |- ( 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:  biimpri  131  bitr2i  183  bitr3i  184  bitr4i  185  syl5bbr  192  syl5rbbr  193  syl6bbr  196  syl6rbbr  197  pm5.41  249  anidm  388  pm4.87  524  anabs1  537  anabs7  539  pm4.76  569  mtbir  629  sylnibr  635  sylnbir  637  xchnxbir  639  xchbinxr  641  nbn  648  pm4.25  708  pm4.77  746  pm4.56  840  pm3.2an3  1118  syl3anbr  1214  3an6  1254  truan  1302  truimfal  1342  nottru  1345  sbid  1698  cleljust  1855  sb10f  1913  necon3bbii  2283  rspc2gv  2713  alexeq  2722  ceqsrexbv  2727  clel2  2729  clel4  2732  dfsbcq2  2819  cbvreucsf  2967  raldifb  3113  difab  3240  un0  3285  in0  3286  ss0b  3290  iindif2m  3753  epse  4105  uniuni  4209  cotr  4736  issref  4737  mptpreima  4844  ralrnmpt  5341  rexrnmpt  5342  eroveu  6263  bdeq  10772  bd0r  10774  bdcriota  10832  bj-d0clsepcl  10878  bj-dfom  10886