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  syl6bbr  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  1261  3an6  1301  truan  1349  truimfal  1389  nottru  1392  sbid  1748  cleljust  1911  sb10f  1971  necon3bbii  2346  rspc2gv  2805  alexeq  2815  ceqsrexbv  2820  clel2  2822  clel4  2825  dfsbcq2  2916  cbvreucsf  3069  dfdif3  3191  raldifb  3221  difab  3350  un0  3401  in0  3402  ss0b  3407  rexdifpr  3560  iindif2m  3888  epse  4272  abnex  4376  uniuni  4380  elco  4713  cotr  4928  issref  4929  mptpreima  5040  ralrnmpt  5570  rexrnmpt  5571  eroveu  6528  fprodseq  11384  toptopon  12224  xmeterval  12643  txmetcnp  12726  dedekindicclemicc  12818  eldvap  12859  bdeq  13192  bd0r  13194  bdcriota  13252  bj-d0clsepcl  13294  bj-dfom  13302