Theorem bicomi 123

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 122	. 2 ⊢ ((φ ↔ ψ) → (ψ ↔ φ))
3	1, 2	ax-mp 7	1 ⊢ (ψ ↔ φ)

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimpri  124  bitr2i  174  bitr3i  175  bitr4i  176  syl5bbr  183  syl5rbbr  184  syl6bbr  187  syl6rbbr  188  pm5.41  240  anidm  376  pm4.87  493  anabs1  506  anabs7  508  pm4.76  536  mtbir  595  sylnibr  601  sylnbir  603  xchnxbir  605  xchbinxr  607  nbn  614  pm4.25  674  pm4.77  711  pm4.56  805  pm3.2an3  1082  syl3anbr  1178  3an6  1216  truan  1259  truimfal  1298  nottru  1301  sbid  1654  cleljust  1810  sb10f  1868  necon3bbii  2236  alexeq  2664  ceqsrexbv  2669  clel2  2671  clel4  2674  dfsbcq2  2761  cbvreucsf  2904  raldifb  3077  difab  3200  un0  3245  in0  3246  ss0b  3250  iindif2m  3715  epse  4064  uniuni  4149  cotr  4649  issref  4650  mptpreima  4757  ralrnmpt  5252  rexrnmpt  5253  eroveu  6133  bdeq  9278  bd0r  9280  bdcriota  9338  bj-d0clsepcl  9384  bj-dfom  9392