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  673  sylnibr  679  sylnbir  681  xchnxbir  683  xchbinxr  685  nbn  701  pm4.25  760  pm4.56  782  pm4.77  801  pm3.2an3  1179  syl3anbr  1294  3an6  1335  truan  1390  truimfal  1430  nottru  1433  sbid  1798  sb10f  2024  cleljust  2184  eqabdv  2336  nfabdw  2369  necon3bbii  2415  rspc2gv  2896  alexeq  2906  ceqsrexbv  2911  clel2  2913  clel4  2916  dfsbcq2  3008  cbvreucsf  3166  dfdif3  3291  raldifb  3321  difab  3450  un0  3502  in0  3503  ss0b  3508  rexdifpr  3671  snssb  3777  snssg  3778  iindif2m  4009  epse  4407  abnex  4512  uniuni  4516  elco  4862  cotr  5083  issref  5084  mptpreima  5195  ralrnmpt  5745  rexrnmpt  5746  eroveu  6736  wrd2ind  11214  fprodseq  12009  issrg  13842  toptopon  14605  xmeterval  15022  txmetcnp  15105  dedekindicclemicc  15219  eldvap  15269  fsumdvdsmul  15578  if0ab  15941  bdeq  15958  bd0r  15960  bdcriota  16018  bj-d0clsepcl  16060  bj-dfom  16068