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  557  anabs1  572  anabs7  574  pm4.76  604  mtbir  672  sylnibr  678  sylnbir  680  xchnxbir  682  xchbinxr  684  nbn  700  pm4.25  759  pm4.56  781  pm4.77  800  pm3.2an3  1178  syl3anbr  1293  3an6  1333  truan  1381  truimfal  1421  nottru  1424  sbid  1785  sb10f  2011  cleljust  2170  eqabdv  2322  nfabdw  2355  necon3bbii  2401  rspc2gv  2876  alexeq  2886  ceqsrexbv  2891  clel2  2893  clel4  2896  dfsbcq2  2988  cbvreucsf  3145  dfdif3  3269  raldifb  3299  difab  3428  un0  3480  in0  3481  ss0b  3486  rexdifpr  3646  snssb  3751  snssg  3752  iindif2m  3980  epse  4373  abnex  4478  uniuni  4482  elco  4828  cotr  5047  issref  5048  mptpreima  5159  ralrnmpt  5700  rexrnmpt  5701  eroveu  6680  fprodseq  11726  issrg  13461  toptopon  14186  xmeterval  14603  txmetcnp  14686  dedekindicclemicc  14786  eldvap  14836  if0ab  15297  bdeq  15315  bd0r  15317  bdcriota  15375  bj-d0clsepcl  15417  bj-dfom  15425