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  673  sylnibr  679  sylnbir  681  xchnxbir  683  xchbinxr  685  nbn  701  pm4.25  760  pm4.56  782  pm4.77  801  pm3.2an3  1179  syl3anbr  1294  3an6  1335  truan  1390  truimfal  1430  nottru  1433  sbid  1797  sb10f  2023  cleljust  2182  eqabdv  2334  nfabdw  2367  necon3bbii  2413  rspc2gv  2889  alexeq  2899  ceqsrexbv  2904  clel2  2906  clel4  2909  dfsbcq2  3001  cbvreucsf  3158  dfdif3  3283  raldifb  3313  difab  3442  un0  3494  in0  3495  ss0b  3500  rexdifpr  3661  snssb  3766  snssg  3767  iindif2m  3995  epse  4390  abnex  4495  uniuni  4499  elco  4845  cotr  5065  issref  5066  mptpreima  5177  ralrnmpt  5724  rexrnmpt  5725  eroveu  6715  fprodseq  11927  issrg  13760  toptopon  14523  xmeterval  14940  txmetcnp  15023  dedekindicclemicc  15137  eldvap  15187  fsumdvdsmul  15496  if0ab  15778  bdeq  15796  bd0r  15798  bdcriota  15856  bj-d0clsepcl  15898  bj-dfom  15906