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  703  pm4.25  762  pm4.56  784  pm4.77  803  pm3.2an3  1181  syl3anbr  1296  3an6  1337  truan  1392  truimfal  1432  nottru  1435  sbid  1800  sb10f  2026  cleljust  2186  eqabdv  2338  nfabdw  2371  necon3bbii  2417  rspc2gv  2899  alexeq  2909  ceqsrexbv  2914  clel2  2916  clel4  2919  dfsbcq2  3011  cbvreucsf  3169  dfdif3  3294  raldifb  3324  difab  3453  un0  3505  in0  3506  ss0b  3511  rexdifpr  3674  snssb  3780  snssg  3781  iindif2m  4012  epse  4410  abnex  4515  uniuni  4519  elco  4865  cotr  5086  issref  5087  mptpreima  5198  ralrnmpt  5750  rexrnmpt  5751  eroveu  6743  wrd2ind  11221  fprodseq  12060  issrg  13894  toptopon  14657  xmeterval  15074  txmetcnp  15157  dedekindicclemicc  15271  eldvap  15321  fsumdvdsmul  15630  if0ab  16079  bdeq  16096  bd0r  16098  bdcriota  16156  bj-d0clsepcl  16198  bj-dfom  16206