Theorem bicomi 224

Description: Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
bicomi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bicomi	⊢ (𝜓 ↔ 𝜑)

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bicom1 221	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  biimpri  228  bitr2i  276  bitr3i  277  bitr4i  278  bitr3id  285  bitr3di  286  bitr4di  289  bitr4id  290  mtbir  323  sylnibr  329  sylnbir  331  xchnxbir  333  xchbinxr  335  con1bii  356  nbn  372  xor3  382  pm5.41  390  pm4.63  397  pm4.61  404  pm4.76  518  anidm  564  an21  644  an43  658  anabs1  662  anabs7  664  pm4.87  843  pm4.64  849  pm4.25  905  pm4.77  964  pm4.53  987  pm4.55  989  pm4.56  990  pm4.57  992  pm5.63  1021  3anor  1107  3oran  1108  syl3anbr  1162  3an6  1448  nanbi  1500  nornot  1531  truan  1551  truimfal  1564  nottru  1567  falbitru  1570  nic-dfim  1669  nic-dfneg  1670  2nalexn  1828  2nexaln  1830  equvinv  2029  cleljust  2118  sbelx  2254  sb6rfv  2356  cleljustALT  2363  cleljustALT2  2364  dvelimf  2447  sb5rf  2466  sb6rf  2467  sb10f  2526  nexmo  2535  exists2  2656  cleljustab  2711  eqabdv  2862  eqabcri  2873  nne  2930  necon3bbii  2973  necon2abii  2976  necon2bbii  2977  nnel  3040  r19.41v  3168  r3ex  3177  r19.41  3242  rspc2gv  3601  ceqsrexbv  3625  rabeqcOLD  3660  2reu5lem1  3729  2reu5lem2  3730  2reu5lem3  3731  dfsbcq2  3759  cbvreucsf  3909  nss  4014  dfdif3OLD  4084  symdifass  4228  indifdi  4260  difab  4276  neq0  4318  un0  4360  in0  4361  ss0b  4367  eq0rdv  4373  2nreu  4410  ralidm  4478  ralf0  4480  reuprg  4670  snssb  4749  snssg  4750  ssunsn2  4794  iindif2  5044  eqsnuniex  5319  nssss  5418  snopeqop  5469  dffr6  5597  epse  5623  rnep  5893  cotrgOLDOLD  6085  mptpreima  6214  ralrnmpt  7071  fmptsng  7145  fmptsnd  7146  dff14a  7248  f13dfv  7252  weniso  7332  abnex  7736  uniuni  7741  frpoins3xp3g  8123  xpord3inddlem  8136  eroveu  8788  fsetexb  8840  mapsnend  9010  isfinite2  9252  marypha1lem  9391  marypha2lem4  9396  infcllem  9446  en3lplem2  9573  cantnfp1  9641  carden2  9947  fseqenlem1  9984  iscard3  10053  cardnum  10054  alephinit  10055  cardinfima  10057  alephiso  10058  dfac10b  10100  dfackm  10127  isfin5-2  10351  brdom7disj  10491  brdom6disj  10492  fsuppmapnn0fiubex  13964  hash2prb  14444  hashle2prv  14450  hashtpg  14457  hash3tpb  14467  swrdnnn0nd  14628  wrd2ind  14695  cshwsexaOLD  14797  s4f1o  14891  cotr2g  14949  relexpindlem  15036  lcmfunsnlem2  16617  ncoprmlnprm  16705  vdwapun  16952  cshwsiun  17077  cshwshash  17082  grpss  18893  symgsubmefmnd  19335  pmtrfrn  19395  pmtrrn2  19397  pmtrprfvalrn  19425  issrg  20104  0ringnnzr  20441  acsfn1p  20715  unocv  21596  dsmmacl  21657  pmatcollpw2lem  22671  fvmptnn04if  22743  toptopon  22811  ordtbas2  23085  ordtrest2  23098  xmeterval  24327  isclmp  25004  ovolfcl  25374  eldv  25806  eltayl  26274  musumsum  27109  2sqreu  27374  2sqreunn  27375  2sqreult  27376  2sqreultb  27377  2sqreunnlt  27378  2sqreunnltb  27379  nosupinfsep  27651  umgrislfupgrlem  29056  numedglnl  29078  ausgrusgrb  29099  cplgr3v  29369  vtxd0nedgb  29423  finsumvtxdg2ssteplem1  29480  isrgr  29494  rgrusgrprc  29524  rgrprcx  29527  upgr2wlk  29603  dfpth2  29666  wwlksnwwlksnon  29852  usgr2wspthon  29902  isclwwlk  29920  clwwlkvbij  30049  iseupthf1o  30138  frcond2  30203  nfrgr2v  30208  4cycl2vnunb  30226  fusgr2wsp2nb  30270  frgrregord013  30331  lejdii  31474  mdslle1i  32253  mdslle2i  32254  mdslj1i  32255  mdslj2i  32256  mo5f  32425  n0nsnel  32451  unipreima  32574  2ndpreima  32638  mgccnv  32932  quslsm  33383  ordtrest2NEW  33920  ordtconnlem1  33921  ballotlem2  34487  plymulx0  34545  bnj115  34722  bnj156  34725  bnj206  34728  bnj110  34855  bnj121  34867  bnj124  34868  bnj130  34871  bnj153  34877  bnj207  34878  bnj581  34905  bnj611  34915  bnj864  34919  bnj865  34920  bnj893  34925  bnj1000  34938  bnj978  34946  bnj1040  34969  bnj1049  34971  bnj1133  34986  bnj1189  35006  satfv1  35357  satfvsucsuc  35359  satfdm  35363  satf0  35366  satf0op  35371  fmlafvel  35379  cnvco1  35753  cnvco2  35754  dfiota3  35918  ss-ax8  36220  trer  36311  nabi1i  36389  nabi2i  36390  bj-hbext  36705  bj-nnfbit  36747  bj-dvelimdv  36846  bj-gabima  36935  bj-elsngl  36963  bj-nuliotaALT  37053  bj-rest10  37083  bj-restuni  37092  con1bii2  37327  con2bii2  37328  topdifinfeq  37345  isbasisrelowllem2  37351  wl-1xor  37477  wl-1mintru1  37483  wl-sb8eut  37573  wl-sb8eutv  37574  inixp  37729  notbinot1  38080  notbinot2  38084  truconj  38102  sbccom2lem  38125  sbccom2  38126  sbccom2f  38127  tsim1  38131  tsxo3  38140  tsxo4  38141  trcoss2  38482  dfcomember3  38673  eqvreldmqs  38674  eqvreldmqs2  38675  dfmembpart2  38769  eldisjn0el  38805  isopos  39180  islvol5  39580  elpadd0  39810  dvhopellsm  41118  diblsmopel  41172  mapdvalc  41630  3factsumint2  42017  3factsumint3  42018  3factsumint4  42019  aks4d1p1p2  42065  aks4d1p7  42078  isprimroot  42088  aks6d1c1p1  42102  aks6d1c2p2  42114  sticksstones22  42163  unitscyglem4  42193  elpwbi  42225  redvmptabs  42355  dffltz  42629  rmxypairf1o  42907  onsupmaxb  43235  ifpnotnotb  43475  ifpdfxor  43483  ifpidg  43487  ifpim123g  43496  ifpim1g  43497  ifpimimb  43500  ifpimim  43505  rp-fakeanorass  43509  elmapintrab  43572  undmrnresiss  43600  clcnvlem  43619  sqrtcvallem1  43627  cnviun  43646  dfxor4  43762  dfhe3  43771  dffrege69  43928  dffrege76  43935  or3or  44019  uneqsn  44021  scottabf  44236  mnurndlem1  44277  ismnushort  44297  pm10.252  44357  pm10.253  44358  pm10.42  44360  aaanv  44384  pm13.195  44409  pm13.196a  44410  sbc3or  44529  en3lpVD  44841  3orbi123VD  44846  sbc3orgVD  44847  sbcoreleleqVD  44855  undif3VD  44878  ax6e2ndeqVD  44905  ax6e2ndeqALT  44927  sineq0ALT  44933  n0abso  44973  permaxsep  45004  permaxinf2lem  45009  uzwo4  45054  iindif2f  45161  allbutfiinf  45423  limsupequzmptlem  45733  cncfshift  45879  dvnmul  45948  dvnprodlem2  45952  rrxsnicc  46305  salexct  46339  sge00  46381  sge0iunmpt  46423  meadjiun  46471  carageneld  46507  ovncvrrp  46569  ovolval4lem1  46654  vonioo  46687  vonicc  46690  nsssmfmbf  46784  smfmullem4  46799  aibandbiaiffaiffb  46899  plcofph  46949  pldofph  46950  plvcofph  46951  plvcofphax  46952  plvofpos  46953  n0nsn2el  47030  fsetsniunop  47054  2reu8i  47118  aovov0bi  47201  tz6.12-afv2  47245  4an21  47275  ichbi12i  47465  ichnfimlem  47468  spr0nelg  47481  sprvalpwn0  47488  reuprpr  47528  requad2  47628  clnbgrel  47833  usgrexmpl2nb4  48030  pg4cyclnex  48121  copisnmnd  48161  pgrpgt2nabl  48358  lindslinindsimp2lem5  48455  islininds2  48477  ldepslinc  48502  line2ylem  48744