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  596  sylnibr  602  sylnbir  604  xchnxbir  606  xchbinxr  608  nbn  615  pm4.25  675  pm4.77  712  pm4.56  806  pm3.2an3  1083  syl3anbr  1179  3an6  1217  truan  1260  truimfal  1301  nottru  1304  sbid  1657  cleljust  1813  sb10f  1871  necon3bbii  2242  alexeq  2670  ceqsrexbv  2675  clel2  2677  clel4  2680  dfsbcq2  2767  cbvreucsf  2910  raldifb  3083  difab  3206  un0  3251  in0  3252  ss0b  3256  iindif2m  3724  epse  4079  uniuni  4183  cotr  4706  issref  4707  mptpreima  4814  ralrnmpt  5309  rexrnmpt  5310  eroveu  6197  bdeq  9943  bd0r  9945  bdcriota  10003  bj-d0clsepcl  10049  bj-dfom  10057