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  645  an43  659  anabs1  663  anabs7  665  pm4.87  844  pm4.64  850  pm4.25  906  pm4.77  965  pm4.53  988  pm4.55  990  pm4.56  991  pm4.57  993  pm5.63  1022  3anor  1108  3oran  1109  syl3anbr  1163  3an6  1449  nanbi  1502  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1671  nic-dfneg  1672  2nalexn  1830  2nexaln  1832  equvinv  2031  cleljust  2123  sbelx  2261  sb6rfv  2362  cleljustALT  2369  cleljustALT2  2370  dvelimf  2453  sb5rf  2472  sb6rf  2473  sb10f  2532  nexmo  2542  exists2  2663  cleljustab  2718  eqabdv  2870  eqabcri  2880  nne  2937  necon3bbii  2980  necon2abii  2983  necon2bbii  2984  nnel  3047  r19.41v  3168  r3ex  3177  r19.41  3242  rspc2gv  3575  ceqsrexbv  3599  2reu5lem1  3702  2reu5lem2  3703  2reu5lem3  3704  dfsbcq2  3732  cbvreucsf  3882  nss  3987  dfdif3OLD  4059  symdifass  4203  indifdi  4235  difab  4251  neq0  4293  un0  4335  in0  4336  ss0b  4342  2nreu  4385  ralidm  4458  reuprg  4648  snssb  4727  snssg  4728  ssunsn2  4771  iindif2  5020  eqsnuniex  5302  nssss  5406  snopeqop  5458  dffr6  5584  epse  5610  rnep  5880  mptpreima  6200  ralrnmpt  7046  fmptsng  7120  fmptsnd  7121  dff14a  7222  f13dfv  7226  weniso  7306  abnex  7708  uniuni  7713  frpoins3xp3g  8088  xpord3inddlem  8101  eroveu  8756  fsetexb  8808  mapsnend  8980  isfinite2  9205  marypha1lem  9343  marypha2lem4  9348  infcllem  9398  en3lplem2  9531  cantnfp1  9599  carden2  9908  fseqenlem1  9943  iscard3  10012  cardnum  10013  alephinit  10014  cardinfima  10016  alephiso  10017  dfac10b  10059  dfackm  10086  isfin5-2  10310  brdom7disj  10450  brdom6disj  10451  fsuppmapnn0fiubex  13951  hash2prb  14431  hashle2prv  14437  hashtpg  14444  hash3tpb  14454  swrdnnn0nd  14616  wrd2ind  14682  s4f1o  14877  cotr2g  14935  relexpindlem  15022  lcmfunsnlem2  16606  ncoprmlnprm  16695  vdwapun  16942  cshwsiun  17067  cshwshash  17072  grpss  18927  symgsubmefmnd  19370  pmtrfrn  19430  pmtrrn2  19432  pmtrprfvalrn  19460  issrg  20166  0ringnnzr  20499  acsfn1p  20773  unocv  21657  dsmmacl  21718  pmatcollpw2lem  22739  fvmptnn04if  22811  toptopon  22879  ordtbas2  23153  ordtrest2  23166  xmeterval  24394  isclmp  25061  ovolfcl  25430  eldv  25862  eltayl  26322  musumsum  27152  2sqreu  27416  2sqreunn  27417  2sqreult  27418  2sqreultb  27419  2sqreunnlt  27420  2sqreunnltb  27421  nosupinfsep  27693  umgrislfupgrlem  29188  numedglnl  29210  ausgrusgrb  29231  cplgr3v  29501  vtxd0nedgb  29554  finsumvtxdg2ssteplem1  29611  isrgr  29625  rgrusgrprc  29655  rgrprcx  29658  upgr2wlk  29732  dfpth2  29794  wwlksnwwlksnon  29980  usgr2wspthon  30033  isclwwlk  30051  clwwlkvbij  30180  iseupthf1o  30269  frcond2  30334  nfrgr2v  30339  4cycl2vnunb  30357  fusgr2wsp2nb  30401  frgrregord013  30462  lejdii  31606  mdslle1i  32385  mdslle2i  32386  mdslj1i  32387  mdslj2i  32388  mo5f  32555  n0nsnel  32582  unipreima  32713  2ndpreima  32778  mgccnv  33056  domnprodeq0  33334  quslsm  33462  mplmonprod  33695  ordtrest2NEW  34064  ordtconnlem1  34065  ballotlem2  34630  plymulx0  34688  bnj115  34865  bnj156  34868  bnj206  34871  bnj110  34997  bnj121  35009  bnj124  35010  bnj130  35013  bnj153  35019  bnj207  35020  bnj581  35047  bnj611  35057  bnj864  35061  bnj865  35062  bnj893  35067  bnj1000  35080  bnj978  35088  bnj1040  35111  bnj1049  35113  bnj1133  35128  bnj1189  35148  satfv1  35542  satfvsucsuc  35544  satfdm  35548  satf0  35551  satf0op  35556  fmlafvel  35564  cnvco1  35938  cnvco2  35939  dfiota3  36100  ss-ax8  36404  trer  36495  nabi1i  36573  nabi2i  36574  regsfromregtco  36717  bj-nnfbit  37052  bj-dvelimdv  37155  bj-gabima  37244  bj-elsngl  37272  bj-nuliotaALT  37362  bj-axseprep  37378  bj-rest10  37397  bj-restuni  37406  con1bii2  37645  con2bii2  37646  topdifinfeq  37663  isbasisrelowllem2  37669  wl-1xor  37795  wl-1mintru1  37801  wl-sb8eut  37900  wl-sb8eutv  37901  inixp  38046  notbinot1  38397  notbinot2  38401  truconj  38419  sbccom2lem  38442  sbccom2  38443  sbccom2f  38444  tsim1  38448  tsxo3  38457  tsxo4  38458  trcoss2  38892  dfcomember3  39077  eqvreldmqs  39078  eqvreldmqs2  39079  dfmembpart2  39191  eldisjn0el  39227  isopos  39623  islvol5  40022  elpadd0  40252  dvhopellsm  41560  diblsmopel  41614  mapdvalc  42072  3factsumint2  42458  3factsumint3  42459  3factsumint4  42460  aks4d1p1p2  42506  aks4d1p7  42519  isprimroot  42529  aks6d1c1p1  42543  aks6d1c2p2  42555  sticksstones22  42604  unitscyglem4  42634  elpwbi  42668  redvmptabs  42789  dffltz  43064  rmxypairf1o  43336  onsupmaxb  43664  ifpnotnotb  43903  ifpdfxor  43911  ifpidg  43915  ifpim123g  43924  ifpim1g  43925  ifpimimb  43928  ifpimim  43933  rp-fakeanorass  43937  elmapintrab  44000  undmrnresiss  44028  clcnvlem  44047  sqrtcvallem1  44055  cnviun  44074  dfxor4  44190  dfhe3  44199  dffrege69  44356  dffrege76  44363  or3or  44447  uneqsn  44449  scottabf  44664  mnurndlem1  44705  ismnushort  44725  pm10.252  44785  pm10.253  44786  pm10.42  44788  aaanv  44812  pm13.195  44837  pm13.196a  44838  sbc3or  44956  en3lpVD  45268  3orbi123VD  45273  sbc3orgVD  45274  sbcoreleleqVD  45282  undif3VD  45305  ax6e2ndeqVD  45332  ax6e2ndeqALT  45354  sineq0ALT  45360  n0abso  45400  permaxsep  45431  permaxinf2lem  45436  uzwo4  45481  iindif2f  45587  allbutfiinf  45845  limsupequzmptlem  46153  cncfshift  46299  dvnmul  46368  dvnprodlem2  46372  rrxsnicc  46725  salexct  46759  sge00  46801  sge0iunmpt  46843  meadjiun  46891  carageneld  46927  ovncvrrp  46989  ovolval4lem1  47074  vonioo  47107  vonicc  47110  nsssmfmbf  47204  smfmullem4  47219  aibandbiaiffaiffb  47333  plcofph  47383  pldofph  47384  plvcofph  47385  plvcofphax  47386  plvofpos  47387  n0nsn2el  47464  fsetsniunop  47488  2reu8i  47552  aovov0bi  47635  tz6.12-afv2  47679  4an21  47709  ichbi12i  47911  ichnfimlem  47914  spr0nelg  47927  sprvalpwn0  47934  reuprpr  47974  nprmmul1  47978  requad2  48090  clnbgrel  48295  usgrexmpl2nb4  48502  pg4cyclnex  48594  copisnmnd  48636  pgrpgt2nabl  48833  lindslinindsimp2lem5  48929  islininds2  48951  ldepslinc  48976  line2ylem  49218