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  1788  sb10f  2014  cleljust  2173  eqabdv  2325  nfabdw  2358  necon3bbii  2404  rspc2gv  2880  alexeq  2890  ceqsrexbv  2895  clel2  2897  clel4  2900  dfsbcq2  2992  cbvreucsf  3149  dfdif3  3274  raldifb  3304  difab  3433  un0  3485  in0  3486  ss0b  3491  rexdifpr  3651  snssb  3756  snssg  3757  iindif2m  3985  epse  4378  abnex  4483  uniuni  4487  elco  4833  cotr  5052  issref  5053  mptpreima  5164  ralrnmpt  5707  rexrnmpt  5708  eroveu  6694  fprodseq  11765  issrg  13597  toptopon  14338  xmeterval  14755  txmetcnp  14838  dedekindicclemicc  14952  eldvap  15002  fsumdvdsmul  15311  if0ab  15535  bdeq  15553  bd0r  15555  bdcriota  15613  bj-d0clsepcl  15655  bj-dfom  15663