Theorem bicomi 193

Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
bicomi.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
bicomi	⊢ (ψ ↔ φ)

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 ⊢ (φ ↔ ψ)
2		bicom1 190	. 2 ⊢ ((φ ↔ ψ) → (ψ ↔ φ))
3	1, 2	ax-mp 5	1 ⊢ (ψ ↔ φ)

Syntax hints:   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimpri  197  bitr2i  241  bitr3i  242  bitr4i  243  syl5bbr  250  syl5rbbr  251  syl6bbr  254  syl6rbbr  255  mtbir  290  sylnibr  296  sylnbir  298  xchnxbir  300  xchbinxr  302  con1bii  321  con2bii  322  nbn  336  xor3  346  pm5.41  353  pm4.64  361  pm4.63  410  pm4.61  415  anor  475  pm4.53  478  pm4.55  480  pm4.56  481  pm4.57  483  pm4.25  501  pm4.87  567  anidm  625  pm4.77  762  anabs1  783  anabs7  785  pm4.76  836  pm5.63  890  3ianor  949  3oran  951  pm3.2an3  1131  syl3anbr  1226  3an6  1262  nannot  1293  truimfal  1345  nottru  1348  nic-dfim  1434  nic-dfneg  1435  2nalexn  1573  sbid  1922  dvelimf  1997  cleljust  2014  cleljustALT  2015  sb10f  2122  nne  2520  necon3bbii  2547  necon2abii  2571  necon2bbii  2572  alexeq  2968  ceqsrexbv  2973  clel2  2975  clel4  2978  2reu5lem1  3041  2reu5lem2  3042  2reu5lem3  3043  dfsbcq2  3049  cbvreucsf  3200  nss  3329  difab  3523  un0  3575  in0  3576  ss0b  3580  ssunsn2  3865  iindif2  4035  nnsucelrlem1  4424  dfop2  4575  brex  4689  dmuni  4914  brelrn  4960  elimasn  5019  funun  5146  rnoprab  5576  mptpreima  5682  rnmpt2  5717  dmtxp  5802  nncdiv3lem2  6276  nchoicelem11  6299  epelcres  6328