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  523  anabs1  536  anabs7  538  pm4.76  568  mtbir  628  sylnibr  634  sylnbir  636  xchnxbir  638  xchbinxr  640  nbn  647  pm4.25  707  pm4.77  745  pm4.56  839  pm3.2an3  1117  syl3anbr  1213  3an6  1253  truan  1301  truimfal  1341  nottru  1344  sbid  1697  cleljust  1854  sb10f  1912  necon3bbii  2282  rspc2gv  2712  alexeq  2721  ceqsrexbv  2726  clel2  2728  clel4  2731  dfsbcq2  2818  cbvreucsf  2966  raldifb  3112  difab  3233  un0  3278  in0  3279  ss0b  3283  iindif2m  3745  epse  4097  uniuni  4201  cotr  4726  issref  4727  mptpreima  4834  ralrnmpt  5330  rexrnmpt  5331  eroveu  6220  bdeq  10614  bd0r  10616  bdcriota  10674  bj-d0clsepcl  10720  bj-dfom  10728