Theorem bicomi 193

Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimpri  197  bitr2i  241  bitr3i  242  bitr4i  243  syl5bbr  250  syl5rbbr  251  syl6bbr  254  syl6rbbr  255  mtbir  290  sylnibr  296  sylnbir  298  xchnxbir  300  xchbinxr  302  con1bii  321  con2bii  322  nbn  336  xor3  346  pm5.41  353  pm4.64  361  pm4.63  410  pm4.61  415  anor  475  pm4.53  478  pm4.55  480  pm4.56  481  pm4.57  483  pm4.25  501  pm4.87  567  anidm  625  pm4.77  762  anabs1  783  anabs7  785  pm4.76  836  pm5.63  890  3ianor  949  3oran  951  pm3.2an3  1131  syl3anbr  1226  3an6  1262  nannot  1293  truimfal  1345  nottru  1348  nic-dfim  1434  nic-dfneg  1435  2nalexn  1573  sbid  1922  dvelimf  1997  cleljust  2014  cleljustALT  2015  sb10f  2122  nne  2521  necon3bbii  2548  necon2abii  2572  necon2bbii  2573  alexeq  2969  ceqsrexbv  2974  clel2  2976  clel4  2979  2reu5lem1  3042  2reu5lem2  3043  2reu5lem3  3044  dfsbcq2  3050  cbvreucsf  3201  nss  3330  difab  3524  un0  3576  in0  3577  ss0b  3581  ssunsn2  3866  iindif2  4036  nnsucelrlem1  4425  dfop2  4576  brex  4690  dmuni  4915  brelrn  4961  elimasn  5020  funun  5147  rnoprab  5577  mptpreima  5683  rnmpt2  5718  dmtxp  5803  nncdiv3lem2  6277  nchoicelem11  6300  epelcres  6329