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  400  an21  475  pm4.87  563  anabs1  578  anabs7  580  an43  594  pm4.76  612  mtbir  682  sylnibr  688  sylnbir  690  xchnxbir  692  xchbinxr  694  nbn  711  pm4.25  770  pm4.56  792  pm4.77  811  pm3.2an3  1207  syl3anbr  1322  3an6  1363  truan  1419  truimfal  1459  nottru  1462  sbid  1827  sb10f  2055  cleljust  2215  eqabdv  2369  nfabdw  2411  necon3bbii  2457  rspc2gv  2942  alexeq  2952  ceqsrexbv  2957  clel2  2959  clel4  2962  dfsbcq2  3054  cbvreucsf  3212  dfdif3  3339  raldifb  3369  difab  3500  un0  3556  in0  3557  ss0b  3562  rexdifpr  3736  snssb  3846  snssg  3847  iindif2m  4078  epse  4485  abnex  4591  uniuni  4595  elco  4944  cotr  5167  issref  5168  mptpreima  5279  ralrnmpt  5844  rexrnmpt  5845  eroveu  6894  mapsnend  7093  wrd2ind  11478  fprodseq  12333  issrg  14252  toptopon  15102  xmeterval  15519  txmetcnp  15602  dedekindicclemicc  15716  eldvap  15766  fsumdvdsmul  16088  isclwwlk  16618  iseupthf1o  16672  eupth2lem1  16682  bdeq  16832  bd0r  16834  bdcriota  16892  bj-d0clsepcl  16934  bj-dfom  16942  alsanmo  17125  ralsanmo  17126  alsralrex  17127  alsraln0m  17128