Theorem bicomi 132

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpri  133  bitr2i  185  bitr3i  186  bitr4i  187  bitr3id  194  bitr3di  195  bitr4di  198  bitr4id  199  pm5.41  251  anidm  396  an21  471  pm4.87  559  anabs1  574  anabs7  576  an43  590  pm4.76  608  mtbir  677  sylnibr  683  sylnbir  685  xchnxbir  687  xchbinxr  689  nbn  706  pm4.25  765  pm4.56  787  pm4.77  806  pm3.2an3  1202  syl3anbr  1317  3an6  1358  truan  1414  truimfal  1454  nottru  1457  sbid  1822  sb10f  2048  cleljust  2208  eqabdv  2360  nfabdw  2393  necon3bbii  2439  rspc2gv  2922  alexeq  2932  ceqsrexbv  2937  clel2  2939  clel4  2942  dfsbcq2  3034  cbvreucsf  3192  dfdif3  3317  raldifb  3347  difab  3476  un0  3528  in0  3529  ss0b  3534  rexdifpr  3697  snssb  3806  snssg  3807  iindif2m  4038  epse  4439  abnex  4544  uniuni  4548  elco  4896  cotr  5118  issref  5119  mptpreima  5230  ralrnmpt  5789  rexrnmpt  5790  eroveu  6795  wrd2ind  11308  fprodseq  12162  issrg  13997  toptopon  14761  xmeterval  15178  txmetcnp  15261  dedekindicclemicc  15375  eldvap  15425  fsumdvdsmul  15734  isclwwlk  16264  iseupthf1o  16318  eupth2lem1  16328  if0ab  16452  bdeq  16469  bd0r  16471  bdcriota  16529  bj-d0clsepcl  16571  bj-dfom  16579