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  678  sylnibr  684  sylnbir  686  xchnxbir  688  xchbinxr  690  nbn  707  pm4.25  766  pm4.56  788  pm4.77  807  pm3.2an3  1203  syl3anbr  1318  3an6  1359  truan  1415  truimfal  1455  nottru  1458  sbid  1823  sb10f  2051  cleljust  2211  eqabdv  2365  nfabdw  2405  necon3bbii  2451  rspc2gv  2935  alexeq  2945  ceqsrexbv  2950  clel2  2952  clel4  2955  dfsbcq2  3047  cbvreucsf  3205  dfdif3  3331  raldifb  3361  difab  3492  un0  3544  in0  3545  ss0b  3550  rexdifpr  3719  snssb  3829  snssg  3830  iindif2m  4061  epse  4465  abnex  4570  uniuni  4574  elco  4923  cotr  5146  issref  5147  mptpreima  5258  ralrnmpt  5821  rexrnmpt  5822  eroveu  6862  mapsnend  7054  wrd2ind  11423  fprodseq  12277  issrg  14130  toptopon  14932  xmeterval  15349  txmetcnp  15432  dedekindicclemicc  15546  eldvap  15596  fsumdvdsmul  15908  isclwwlk  16438  iseupthf1o  16492  eupth2lem1  16502  bdeq  16642  bd0r  16644  bdcriota  16702  bj-d0clsepcl  16744  bj-dfom  16752