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  bitr3id  193  bitr3di  194  bitr4di  197  bitr4id  198  pm5.41  250  anidm  394  pm4.87  547  anabs1  562  anabs7  564  pm4.76  594  mtbir  661  sylnibr  667  sylnbir  669  xchnxbir  671  xchbinxr  673  nbn  689  pm4.25  748  pm4.56  770  pm4.77  789  pm3.2an3  1161  syl3anbr  1264  3an6  1304  truan  1352  truimfal  1392  nottru  1395  sbid  1754  sb10f  1975  cleljust  2134  nfabdw  2318  necon3bbii  2364  rspc2gv  2828  alexeq  2838  ceqsrexbv  2843  clel2  2845  clel4  2848  dfsbcq2  2940  cbvreucsf  3095  dfdif3  3217  raldifb  3247  difab  3376  un0  3427  in0  3428  ss0b  3433  rexdifpr  3588  iindif2m  3916  epse  4302  abnex  4407  uniuni  4411  elco  4752  cotr  4967  issref  4968  mptpreima  5079  ralrnmpt  5609  rexrnmpt  5610  eroveu  6571  fprodseq  11480  toptopon  12427  xmeterval  12846  txmetcnp  12929  dedekindicclemicc  13021  eldvap  13062  if0ab  13391  bdeq  13409  bd0r  13411  bdcriota  13469  bj-d0clsepcl  13511  bj-dfom  13519