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  672  sylnibr  678  sylnbir  680  xchnxbir  682  xchbinxr  684  nbn  700  pm4.25  759  pm4.56  781  pm4.77  800  pm3.2an3  1178  syl3anbr  1293  3an6  1333  truan  1381  truimfal  1421  nottru  1424  sbid  1785  sb10f  2011  cleljust  2170  eqabdv  2322  nfabdw  2355  necon3bbii  2401  rspc2gv  2877  alexeq  2887  ceqsrexbv  2892  clel2  2894  clel4  2897  dfsbcq2  2989  cbvreucsf  3146  dfdif3  3270  raldifb  3300  difab  3429  un0  3481  in0  3482  ss0b  3487  rexdifpr  3647  snssb  3752  snssg  3753  iindif2m  3981  epse  4374  abnex  4479  uniuni  4483  elco  4829  cotr  5048  issref  5049  mptpreima  5160  ralrnmpt  5701  rexrnmpt  5702  eroveu  6682  fprodseq  11729  issrg  13464  toptopon  14197  xmeterval  14614  txmetcnp  14697  dedekindicclemicc  14811  eldvap  14861  if0ab  15367  bdeq  15385  bd0r  15387  bdcriota  15445  bj-d0clsepcl  15487  bj-dfom  15495