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  6904  mapsnend  7103  wrd2ind  11517  fprodseq  12375  issrg  14376  toptopon  15244  xmeterval  15661  txmetcnp  15744  dedekindicclemicc  15858  eldvap  15908  fsumdvdsmul  16285  isclwwlk  16840  iseupthf1o  16894  eupth2lem1  16904  bdeq  17054  bd0r  17056  bdcriota  17114  bj-d0clsepcl  17156  bj-dfom  17164  alsanmo  17358  ralsanmo  17359  alsralrex  17360  alsraln0m  17361