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  an21  468  pm4.87  552  anabs1  567  anabs7  569  pm4.76  599  mtbir  666  sylnibr  672  sylnbir  674  xchnxbir  676  xchbinxr  678  nbn  694  pm4.25  753  pm4.56  775  pm4.77  794  pm3.2an3  1171  syl3anbr  1277  3an6  1317  truan  1365  truimfal  1405  nottru  1408  sbid  1767  sb10f  1988  cleljust  2147  nfabdw  2331  necon3bbii  2377  rspc2gv  2846  alexeq  2856  ceqsrexbv  2861  clel2  2863  clel4  2866  dfsbcq2  2958  cbvreucsf  3113  dfdif3  3237  raldifb  3267  difab  3396  un0  3448  in0  3449  ss0b  3454  rexdifpr  3611  iindif2m  3940  epse  4327  abnex  4432  uniuni  4436  elco  4777  cotr  4992  issref  4993  mptpreima  5104  ralrnmpt  5638  rexrnmpt  5639  eroveu  6604  fprodseq  11546  toptopon  12810  xmeterval  13229  txmetcnp  13312  dedekindicclemicc  13404  eldvap  13445  if0ab  13840  bdeq  13858  bd0r  13860  bdcriota  13918  bj-d0clsepcl  13960  bj-dfom  13968