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  1823  sb10f  2051  cleljust  2211  eqabdv  2365  nfabdw  2405  necon3bbii  2451  rspc2gv  2936  alexeq  2946  ceqsrexbv  2951  clel2  2953  clel4  2956  dfsbcq2  3048  cbvreucsf  3206  dfdif3  3333  raldifb  3363  difab  3494  un0  3546  in0  3547  ss0b  3552  rexdifpr  3723  snssb  3833  snssg  3834  iindif2m  4065  epse  4469  abnex  4574  uniuni  4578  elco  4927  cotr  5150  issref  5151  mptpreima  5262  ralrnmpt  5825  rexrnmpt  5826  eroveu  6874  mapsnend  7066  wrd2ind  11444  fprodseq  12299  issrg  14213  toptopon  15014  xmeterval  15431  txmetcnp  15514  dedekindicclemicc  15628  eldvap  15678  fsumdvdsmul  15990  isclwwlk  16520  iseupthf1o  16574  eupth2lem1  16584  bdeq  16734  bd0r  16736  bdcriota  16794  bj-d0clsepcl  16836  bj-dfom  16844