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  678  sylnibr  684  sylnbir  686  xchnxbir  688  xchbinxr  690  nbn  707  pm4.25  766  pm4.56  788  pm4.77  807  pm3.2an3  1203  syl3anbr  1318  3an6  1359  truan  1415  truimfal  1455  nottru  1458  sbid  1822  sb10f  2048  cleljust  2208  eqabdv  2361  nfabdw  2394  necon3bbii  2440  rspc2gv  2923  alexeq  2933  ceqsrexbv  2938  clel2  2940  clel4  2943  dfsbcq2  3035  cbvreucsf  3193  dfdif3  3319  raldifb  3349  difab  3478  un0  3530  in0  3531  ss0b  3536  rexdifpr  3701  snssb  3811  snssg  3812  iindif2m  4043  epse  4445  abnex  4550  uniuni  4554  elco  4902  cotr  5125  issref  5126  mptpreima  5237  ralrnmpt  5797  rexrnmpt  5798  eroveu  6838  wrd2ind  11370  fprodseq  12224  issrg  14059  toptopon  14829  xmeterval  15246  txmetcnp  15329  dedekindicclemicc  15443  eldvap  15493  fsumdvdsmul  15805  isclwwlk  16335  iseupthf1o  16389  eupth2lem1  16399  bdeq  16539  bd0r  16541  bdcriota  16599  bj-d0clsepcl  16641  bj-dfom  16649