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  2049  cleljust  2209  eqabdv  2363  nfabdw  2403  necon3bbii  2449  rspc2gv  2933  alexeq  2943  ceqsrexbv  2948  clel2  2950  clel4  2953  dfsbcq2  3045  cbvreucsf  3203  dfdif3  3329  raldifb  3359  difab  3490  un0  3542  in0  3543  ss0b  3548  rexdifpr  3717  snssb  3827  snssg  3828  iindif2m  4059  epse  4463  abnex  4568  uniuni  4572  elco  4921  cotr  5144  issref  5145  mptpreima  5256  ralrnmpt  5819  rexrnmpt  5820  eroveu  6860  mapsnend  7052  wrd2ind  11415  fprodseq  12269  issrg  14109  toptopon  14883  xmeterval  15300  txmetcnp  15383  dedekindicclemicc  15497  eldvap  15547  fsumdvdsmul  15859  isclwwlk  16389  iseupthf1o  16443  eupth2lem1  16453  bdeq  16593  bd0r  16595  bdcriota  16653  bj-d0clsepcl  16695  bj-dfom  16703