Theorem bicomi 132

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

Syntax hints:   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpri  133  bitr2i  185  bitr3i  186  bitr4i  187  bitr3id  194  bitr3di  195  bitr4di  198  bitr4id  199  pm5.41  251  anidm  396  an21  471  pm4.87  557  anabs1  572  anabs7  574  an43  588  pm4.76  606  mtbir  675  sylnibr  681  sylnbir  683  xchnxbir  685  xchbinxr  687  nbn  704  pm4.25  763  pm4.56  785  pm4.77  804  pm3.2an3  1200  syl3anbr  1315  3an6  1356  truan  1412  truimfal  1452  nottru  1455  sbid  1820  sb10f  2046  cleljust  2206  eqabdv  2358  nfabdw  2391  necon3bbii  2437  rspc2gv  2920  alexeq  2930  ceqsrexbv  2935  clel2  2937  clel4  2940  dfsbcq2  3032  cbvreucsf  3190  dfdif3  3315  raldifb  3345  difab  3474  un0  3526  in0  3527  ss0b  3532  rexdifpr  3695  snssb  3804  snssg  3805  iindif2m  4036  epse  4437  abnex  4542  uniuni  4546  elco  4894  cotr  5116  issref  5117  mptpreima  5228  ralrnmpt  5785  rexrnmpt  5786  eroveu  6790  wrd2ind  11297  fprodseq  12137  issrg  13971  toptopon  14735  xmeterval  15152  txmetcnp  15235  dedekindicclemicc  15349  eldvap  15399  fsumdvdsmul  15708  isclwwlk  16203  iseupthf1o  16257  if0ab  16351  bdeq  16368  bd0r  16370  bdcriota  16428  bj-d0clsepcl  16470  bj-dfom  16478