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  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  3733  snssb  3843  snssg  3844  iindif2m  4075  epse  4482  abnex  4588  uniuni  4592  elco  4941  cotr  5164  issref  5165  mptpreima  5276  ralrnmpt  5841  rexrnmpt  5842  eroveu  6890  mapsnend  7089  wrd2ind  11473  fprodseq  12328  issrg  14243  toptopon  15042  xmeterval  15459  txmetcnp  15542  dedekindicclemicc  15656  eldvap  15706  fsumdvdsmul  16019  isclwwlk  16549  iseupthf1o  16603  eupth2lem1  16613  bdeq  16763  bd0r  16765  bdcriota  16823  bj-d0clsepcl  16865  bj-dfom  16873