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  3273  raldifb  3303  difab  3432  un0  3484  in0  3485  ss0b  3490  rexdifpr  3650  snssb  3755  snssg  3756  iindif2m  3984  epse  4377  abnex  4482  uniuni  4486  elco  4832  cotr  5051  issref  5052  mptpreima  5163  ralrnmpt  5704  rexrnmpt  5705  eroveu  6685  fprodseq  11748  issrg  13521  toptopon  14254  xmeterval  14671  txmetcnp  14754  dedekindicclemicc  14868  eldvap  14918  fsumdvdsmul  15227  if0ab  15451  bdeq  15469  bd0r  15471  bdcriota  15529  bj-d0clsepcl  15571  bj-dfom  15579