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  4487  abnex  4593  uniuni  4597  elco  4946  cotr  5169  issref  5170  mptpreima  5281  ralrnmpt  5850  rexrnmpt  5851  eroveu  6900  mapsnend  7099  wrd2ind  11509  fprodseq  12366  issrg  14318  toptopon  15168  xmeterval  15585  txmetcnp  15668  dedekindicclemicc  15782  eldvap  15832  fsumdvdsmul  16186  isclwwlk  16733  iseupthf1o  16787  eupth2lem1  16797  bdeq  16947  bd0r  16949  bdcriota  17007  bj-d0clsepcl  17049  bj-dfom  17057  alsanmo  17249  ralsanmo  17250  alsralrex  17251  alsraln0m  17252