Theorem bicomi 131

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 130	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
3	1, 2	ax-mp 5	1 |- ( ps <-> ph )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpri  132  bitr2i  184  bitr3i  185  bitr4i  186  syl5bbr  193  syl5rbbr  194  syl6bbr  197  syl6rbbr  198  pm5.41  250  anidm  393  pm4.87  546  anabs1  561  anabs7  563  pm4.76  593  mtbir  660  sylnibr  666  sylnbir  668  xchnxbir  670  xchbinxr  672  nbn  688  pm4.25  747  pm4.56  769  pm4.77  788  pm3.2an3  1160  syl3anbr  1260  3an6  1300  truan  1348  truimfal  1388  nottru  1391  sbid  1747  cleljust  1908  sb10f  1968  necon3bbii  2343  rspc2gv  2796  alexeq  2806  ceqsrexbv  2811  clel2  2813  clel4  2816  dfsbcq2  2907  cbvreucsf  3059  dfdif3  3181  raldifb  3211  difab  3340  un0  3391  in0  3392  ss0b  3397  iindif2m  3875  epse  4259  abnex  4363  uniuni  4367  elco  4700  cotr  4915  issref  4916  mptpreima  5027  ralrnmpt  5555  rexrnmpt  5556  eroveu  6513  toptopon  12174  xmeterval  12593  txmetcnp  12676  dedekindicclemicc  12768  eldvap  12809  bdeq  13010  bd0r  13012  bdcriota  13070  bj-d0clsepcl  13112  bj-dfom  13120