Theorem bicomi 131

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 130	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
3	1, 2	ax-mp 5	1 |- ( ps <-> ph )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpri  132  bitr2i  184  bitr3i  185  bitr4i  186  bitr3id  193  bitr3di  194  bitr4di  197  bitr4id  198  pm5.41  250  anidm  394  pm4.87  547  anabs1  562  anabs7  564  pm4.76  594  mtbir  661  sylnibr  667  sylnbir  669  xchnxbir  671  xchbinxr  673  nbn  689  pm4.25  748  pm4.56  770  pm4.77  789  pm3.2an3  1166  syl3anbr  1272  3an6  1312  truan  1360  truimfal  1400  nottru  1403  sbid  1762  sb10f  1983  cleljust  2142  nfabdw  2327  necon3bbii  2373  rspc2gv  2842  alexeq  2852  ceqsrexbv  2857  clel2  2859  clel4  2862  dfsbcq2  2954  cbvreucsf  3109  dfdif3  3232  raldifb  3262  difab  3391  un0  3442  in0  3443  ss0b  3448  rexdifpr  3604  iindif2m  3933  epse  4320  abnex  4425  uniuni  4429  elco  4770  cotr  4985  issref  4986  mptpreima  5097  ralrnmpt  5627  rexrnmpt  5628  eroveu  6592  fprodseq  11524  toptopon  12656  xmeterval  13075  txmetcnp  13158  dedekindicclemicc  13250  eldvap  13291  if0ab  13687  bdeq  13705  bd0r  13707  bdcriota  13765  bj-d0clsepcl  13807  bj-dfom  13815