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  559  anabs1  574  anabs7  576  an43  590  pm4.76  608  mtbir  677  sylnibr  683  sylnbir  685  xchnxbir  687  xchbinxr  689  nbn  706  pm4.25  765  pm4.56  787  pm4.77  806  pm3.2an3  1202  syl3anbr  1317  3an6  1358  truan  1414  truimfal  1454  nottru  1457  sbid  1821  sb10f  2047  cleljust  2207  eqabdv  2359  nfabdw  2392  necon3bbii  2438  rspc2gv  2921  alexeq  2931  ceqsrexbv  2936  clel2  2938  clel4  2941  dfsbcq2  3033  cbvreucsf  3191  dfdif3  3316  raldifb  3346  difab  3475  un0  3527  in0  3528  ss0b  3533  rexdifpr  3698  snssb  3807  snssg  3808  iindif2m  4039  epse  4441  abnex  4546  uniuni  4550  elco  4898  cotr  5120  issref  5121  mptpreima  5232  ralrnmpt  5792  rexrnmpt  5793  eroveu  6800  wrd2ind  11313  fprodseq  12167  issrg  14002  toptopon  14771  xmeterval  15188  txmetcnp  15271  dedekindicclemicc  15385  eldvap  15435  fsumdvdsmul  15744  isclwwlk  16274  iseupthf1o  16328  eupth2lem1  16338  bdeq  16478  bd0r  16480  bdcriota  16538  bj-d0clsepcl  16580  bj-dfom  16588