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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bicomi	⊢ (𝜓 ↔ 𝜑)

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bicom1 131	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

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  671  sylnibr  677  sylnbir  679  xchnxbir  681  xchbinxr  683  nbn  699  pm4.25  758  pm4.56  780  pm4.77  799  pm3.2an3  1176  syl3anbr  1282  3an6  1322  truan  1370  truimfal  1410  nottru  1413  sbid  1772  sb10f  1993  cleljust  2152  nfabdw  2336  necon3bbii  2382  rspc2gv  2851  alexeq  2861  ceqsrexbv  2866  clel2  2868  clel4  2871  dfsbcq2  2963  cbvreucsf  3119  dfdif3  3243  raldifb  3273  difab  3402  un0  3454  in0  3455  ss0b  3460  rexdifpr  3617  snssb  3722  snssg  3723  iindif2m  3949  epse  4336  abnex  4441  uniuni  4445  elco  4786  cotr  5002  issref  5003  mptpreima  5114  ralrnmpt  5650  rexrnmpt  5651  eroveu  6616  fprodseq  11557  issrg  12941  toptopon  13067  xmeterval  13486  txmetcnp  13569  dedekindicclemicc  13661  eldvap  13702  if0ab  14097  bdeq  14115  bd0r  14117  bdcriota  14175  bj-d0clsepcl  14217  bj-dfom  14225