Theorem bicomi 223

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 220	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biimpri  227  bitr2i  275  bitr3i  276  bitr4i  277  bitr3id  284  bitr3di  285  bitr4di  288  bitr4id  289  mtbir  322  sylnibr  328  sylnbir  330  xchnxbir  332  xchbinxr  334  con1bii  356  nbn  372  xor3  383  pm5.41  391  pm4.63  398  pm4.61  405  pm4.76  519  anidm  565  an21  642  an43  656  anabs1  660  anabs7  662  pm4.87  841  pm4.64  847  pm4.25  904  pm4.77  961  pm4.53  984  pm4.55  986  pm4.56  987  pm4.57  989  pm5.63  1018  3anor  1108  3oran  1109  syl3anbr  1162  3an6  1446  nanbi  1498  nornot  1532  truan  1552  truimfal  1565  nottru  1568  falbitru  1571  nic-dfim  1671  nic-dfneg  1672  2nalexn  1830  2nexaln  1832  equvinv  2032  cleljust  2115  sbelx  2245  sb5OLD  2268  sb6rfv  2353  cleljustALT  2360  cleljustALT2  2361  dvelimf  2446  sb5rf  2465  sb6rf  2466  sb10f  2525  nexmo  2534  exists2  2656  cleljustab  2711  eqabdv  2866  eqabcri  2877  nfabdwOLD  2926  nne  2943  necon3bbii  2987  necon2abii  2990  necon2bbii  2991  nnel  3055  nelbOLD  3221  ralcom4OLD  3268  rspc2gv  3590  ceqsrexbv  3609  clel4OLD  3619  rabeqcOLD  3646  2reu5lem1  3716  2reu5lem2  3717  2reu5lem3  3718  dfsbcq2  3745  cbvreucsf  3905  nss  4011  ss2abdv  4025  dfdif3  4079  symdifass  4216  indifdi  4248  difab  4265  neq0  4310  ab0OLD  4340  un0  4355  in0  4356  ss0b  4362  eq0rdv  4369  2nreu  4406  ralidm  4474  ralf0  4476  rexdifpr  4624  reuprg  4669  snssb  4748  snssg  4749  ssunsn2  4792  iindif2  5042  eqsnuniex  5321  nssss  5417  snopeqop  5468  dffr6  5596  epse  5621  rnep  5887  cotrgOLDOLD  6068  mptpreima  6195  ralrnmpt  7051  fmptsng  7119  fmptsnd  7120  dff14a  7222  f13dfv  7225  weniso  7304  abnex  7696  uniuni  7701  frpoins3xp3g  8078  xpord3inddlem  8091  suppvalbr  8101  eroveu  8758  fsetexb  8809  mapsnend  8987  isfinite2  9252  marypha1lem  9378  marypha2lem4  9383  infcllem  9432  en3lplem2  9558  cantnfp1  9626  carden2  9932  fseqenlem1  9969  iscard3  10038  cardnum  10039  alephinit  10040  cardinfima  10042  alephiso  10043  dfac10b  10084  dfackm  10111  isfin5-2  10336  brdom7disj  10476  brdom6disj  10477  fsuppmapnn0fiubex  13907  hash2prb  14383  hashle2prv  14389  hashtpg  14396  swrdnnn0nd  14556  wrd2ind  14623  cshwsexaOLD  14725  s4f1o  14819  cotr2g  14873  relexpindlem  14960  lcmfunsnlem2  16527  ncoprmlnprm  16614  vdwapun  16857  cshwsiun  16983  cshwshash  16988  grpss  18782  symgsubmefmnd  19194  pmtrfrn  19254  pmtrrn2  19256  pmtrprfvalrn  19284  issrg  19933  0ringnnzr  20212  acsfn1p  20322  unocv  21121  dsmmacl  21184  pmatcollpw2lem  22163  fvmptnn04if  22235  toptopon  22303  ordtbas2  22579  ordtrest2  22592  xmeterval  23822  isclmp  24497  ovolfcl  24867  eldv  25299  eltayl  25756  musumsum  26578  2sqreu  26841  2sqreunn  26842  2sqreult  26843  2sqreultb  26844  2sqreunnlt  26845  2sqreunnltb  26846  nosupinfsep  27117  umgrislfupgrlem  28136  numedglnl  28158  ausgrusgrb  28179  cplgr3v  28446  vtxd0nedgb  28499  finsumvtxdg2ssteplem1  28556  isrgr  28570  rgrusgrprc  28600  rgrprcx  28603  upgr2wlk  28679  wwlksnwwlksnon  28923  usgr2wspthon  28973  isclwwlk  28991  clwwlkvbij  29120  iseupthf1o  29209  frcond2  29274  nfrgr2v  29279  4cycl2vnunb  29297  fusgr2wsp2nb  29341  frgrregord013  29402  lejdii  30543  mdslle1i  31322  mdslle2i  31323  mdslj1i  31324  mdslj2i  31325  mo5f  31481  unipreima  31627  2ndpreima  31689  mgccnv  31929  quslsm  32260  ordtrest2NEW  32593  ordtconnlem1  32594  ballotlem2  33177  plymulx0  33248  bnj115  33426  bnj156  33429  bnj206  33432  bnj110  33559  bnj121  33571  bnj124  33572  bnj130  33575  bnj153  33581  bnj207  33582  bnj581  33609  bnj611  33619  bnj864  33623  bnj865  33624  bnj893  33629  bnj1000  33642  bnj978  33650  bnj1040  33673  bnj1049  33675  bnj1133  33690  bnj1189  33710  satfv1  34044  satfvsucsuc  34046  satfdm  34050  satf0  34053  satf0op  34058  fmlafvel  34066  cnvco1  34418  cnvco2  34419  dfiota3  34584  trer  34864  nabi1i  34942  nabi2i  34943  bj-hbext  35251  bj-nnfbit  35293  bj-dvelimdv  35393  bj-gabima  35483  bj-elsngl  35512  bj-nuliotaALT  35602  bj-rest10  35632  bj-restuni  35641  con1bii2  35876  con2bii2  35877  topdifinfeq  35894  isbasisrelowllem2  35900  wl-1xor  36026  wl-1mintru1  36032  wl-sb8eut  36105  inixp  36260  notbinot1  36611  notbinot2  36615  truconj  36633  sbccom2lem  36656  sbccom2  36657  sbccom2f  36658  tsim1  36662  tsxo3  36671  tsxo4  36672  trcoss2  37019  dfcomember3  37209  eqvreldmqs  37210  eqvreldmqs2  37211  dfmembpart2  37305  eldisjn0el  37341  isopos  37715  islvol5  38115  elpadd0  38345  dvhopellsm  39653  diblsmopel  39707  mapdvalc  40165  3factsumint2  40552  3factsumint3  40553  3factsumint4  40554  aks4d1p1p2  40600  aks4d1p7  40613  aks6d1c2p2  40622  sticksstones22  40649  elpwbi  40725  dffltz  41030  rmxypairf1o  41293  onsupmaxb  41631  ifpnotnotb  41873  ifpdfxor  41881  ifpidg  41885  ifpim123g  41894  ifpim1g  41895  ifpimimb  41898  ifpimim  41903  rp-fakeanorass  41907  elmapintrab  41970  undmrnresiss  41998  clcnvlem  42017  sqrtcvallem1  42025  cnviun  42044  dfxor4  42160  dfhe3  42169  dffrege69  42326  dffrege76  42333  or3or  42417  uneqsn  42419  scottabf  42642  mnurndlem1  42683  ismnushort  42703  pm10.252  42763  pm10.253  42764  pm10.42  42766  aaanv  42790  pm13.195  42815  pm13.196a  42816  sbc3or  42936  en3lpVD  43249  3orbi123VD  43254  sbc3orgVD  43255  sbcoreleleqVD  43263  undif3VD  43286  ax6e2ndeqVD  43313  ax6e2ndeqALT  43335  sineq0ALT  43341  uzwo4  43383  iindif2f  43497  fompt  43533  allbutfiinf  43775  limsupequzmptlem  44089  cncfshift  44235  dvnmul  44304  dvnprodlem2  44308  rrxsnicc  44661  salexct  44695  sge00  44737  sge0iunmpt  44779  meadjiun  44827  carageneld  44863  ovncvrrp  44925  ovolval4lem1  45010  vonioo  45043  vonicc  45046  nsssmfmbf  45140  smfmullem4  45155  aibandbiaiffaiffb  45249  plcofph  45299  pldofph  45300  plvcofph  45301  plvcofphax  45302  plvofpos  45303  fsetsniunop  45403  2reu8i  45465  aovov0bi  45548  tz6.12-afv2  45592  4an21  45622  ichbi12i  45772  ichnfimlem  45775  spr0nelg  45788  sprvalpwn0  45795  reuprpr  45835  requad2  45935  copisnmnd  46223  pgrpgt2nabl  46562  lindslinindsimp2lem5  46663  islininds2  46685  ldepslinc  46710  line2ylem  46957