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 ⊢ (𝜓 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpri  133  bitr2i  185  bitr3i  186  bitr4i  187  bitr3id  194  bitr3di  195  bitr4di  198  bitr4id  199  pm5.41  251  anidm  400  an21  475  pm4.87  563  anabs1  578  anabs7  580  an43  594  pm4.76  612  mtbir  682  sylnibr  688  sylnbir  690  xchnxbir  692  xchbinxr  694  nbn  711  pm4.25  770  pm4.56  792  pm4.77  811  pm3.2an3  1207  syl3anbr  1322  3an6  1363  truan  1419  truimfal  1459  nottru  1462  sbid  1827  sb10f  2055  cleljust  2215  eqabdv  2369  nfabdw  2411  necon3bbii  2457  rspc2gv  2942  alexeq  2952  ceqsrexbv  2957  clel2  2959  clel4  2962  dfsbcq2  3054  cbvreucsf  3212  dfdif3  3339  raldifb  3369  difab  3500  un0  3556  in0  3557  ss0b  3562  rexdifpr  3737  snssb  3848  snssg  3849  iindif2m  4080  epse  4489  abnex  4595  uniuni  4599  elco  4948  cotr  5172  issref  5173  mptpreima  5284  ralrnmpt  5853  rexrnmpt  5854  eroveu  6905  mapsnend  7105  wrd2ind  11516  fprodseq  12374  issrg  14375  toptopon  15261  xmeterval  15678  txmetcnp  15761  dedekindicclemicc  15875  eldvap  15925  fsumdvdsmul  16302  isclwwlk  16857  iseupthf1o  16911  eupth2lem1  16921  bdeq  17071  bd0r  17073  bdcriota  17131  bj-d0clsepcl  17173  bj-dfom  17181  alsanmo  17375  ralsanmo  17376  alsralrex  17377  alsraln0m  17378