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  bitr3id  193  bitr3di  194  bitr4di  197  bitr4id  198  pm5.41  250  anidm  394  pm4.87  547  anabs1  562  anabs7  564  pm4.76  594  mtbir  661  sylnibr  667  sylnbir  669  xchnxbir  671  xchbinxr  673  nbn  689  pm4.25  748  pm4.56  770  pm4.77  789  pm3.2an3  1161  syl3anbr  1264  3an6  1304  truan  1352  truimfal  1392  nottru  1395  sbid  1754  sb10f  1975  cleljust  2134  nfabdw  2318  necon3bbii  2364  rspc2gv  2828  alexeq  2838  ceqsrexbv  2843  clel2  2845  clel4  2848  dfsbcq2  2940  cbvreucsf  3095  dfdif3  3217  raldifb  3247  difab  3376  un0  3427  in0  3428  ss0b  3433  rexdifpr  3588  iindif2m  3916  epse  4302  abnex  4406  uniuni  4410  elco  4751  cotr  4966  issref  4967  mptpreima  5078  ralrnmpt  5608  rexrnmpt  5609  eroveu  6568  fprodseq  11473  toptopon  12387  xmeterval  12806  txmetcnp  12889  dedekindicclemicc  12981  eldvap  13022  if0ab  13351  bdeq  13369  bd0r  13371  bdcriota  13429  bj-d0clsepcl  13471  bj-dfom  13479