Theorem bicomi 131

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 130	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpri  132  bitr2i  184  bitr3i  185  bitr4i  186  syl5bbr  193  syl5rbbr  194  syl6bbr  197  syl6rbbr  198  pm5.41  250  anidm  393  pm4.87  546  anabs1  561  anabs7  563  pm4.76  593  mtbir  660  sylnibr  666  sylnbir  668  xchnxbir  670  xchbinxr  672  nbn  688  pm4.25  747  pm4.56  769  pm4.77  788  pm3.2an3  1160  syl3anbr  1260  3an6  1300  truan  1348  truimfal  1388  nottru  1391  sbid  1747  cleljust  1910  sb10f  1970  necon3bbii  2345  rspc2gv  2801  alexeq  2811  ceqsrexbv  2816  clel2  2818  clel4  2821  dfsbcq2  2912  cbvreucsf  3064  dfdif3  3186  raldifb  3216  difab  3345  un0  3396  in0  3397  ss0b  3402  iindif2m  3880  epse  4264  abnex  4368  uniuni  4372  elco  4705  cotr  4920  issref  4921  mptpreima  5032  ralrnmpt  5562  rexrnmpt  5563  eroveu  6520  toptopon  12195  xmeterval  12614  txmetcnp  12697  dedekindicclemicc  12789  eldvap  12830  bdeq  13031  bd0r  13033  bdcriota  13091  bj-d0clsepcl  13133  bj-dfom  13141