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  pm4.76  604  mtbir  671  sylnibr  677  sylnbir  679  xchnxbir  681  xchbinxr  683  nbn  699  pm4.25  758  pm4.56  780  pm4.77  799  pm3.2an3  1176  syl3anbr  1282  3an6  1322  truan  1370  truimfal  1410  nottru  1413  sbid  1774  sb10f  1995  cleljust  2154  nfabdw  2338  necon3bbii  2384  rspc2gv  2853  alexeq  2863  ceqsrexbv  2868  clel2  2870  clel4  2873  dfsbcq2  2965  cbvreucsf  3121  dfdif3  3245  raldifb  3275  difab  3404  un0  3456  in0  3457  ss0b  3462  rexdifpr  3620  snssb  3725  snssg  3726  iindif2m  3954  epse  4342  abnex  4447  uniuni  4451  elco  4793  cotr  5010  issref  5011  mptpreima  5122  ralrnmpt  5658  rexrnmpt  5659  eroveu  6625  fprodseq  11586  issrg  13101  toptopon  13409  xmeterval  13828  txmetcnp  13911  dedekindicclemicc  14003  eldvap  14044  if0ab  14439  bdeq  14457  bd0r  14459  bdcriota  14517  bj-d0clsepcl  14559  bj-dfom  14567