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  2355  cleljustALT  2362  cleljustALT2  2363  dvelimf  2446  sb5rf  2465  sb6rf  2466  sb10f  2525  nexmo  2534  exists2  2655  cleljustab  2710  eqabdv  2861  eqabcri  2872  nne  2929  necon3bbii  2972  necon2abii  2975  necon2bbii  2976  nnel  3039  r19.41v  3165  r3ex  3174  r19.41  3239  rspc2gv  3595  ceqsrexbv  3619  rabeqcOLD  3654  2reu5lem1  3723  2reu5lem2  3724  2reu5lem3  3725  dfsbcq2  3753  cbvreucsf  3903  nss  4008  dfdif3OLD  4077  symdifass  4221  indifdi  4253  difab  4269  neq0  4311  un0  4353  in0  4354  ss0b  4360  eq0rdv  4366  2nreu  4403  ralidm  4471  ralf0  4473  reuprg  4663  snssb  4742  snssg  4743  ssunsn2  4787  iindif2  5036  eqsnuniex  5311  nssss  5410  snopeqop  5461  dffr6  5587  epse  5613  rnep  5880  mptpreima  6199  ralrnmpt  7050  fmptsng  7124  fmptsnd  7125  dff14a  7227  f13dfv  7231  weniso  7311  abnex  7713  uniuni  7718  frpoins3xp3g  8097  xpord3inddlem  8110  eroveu  8762  fsetexb  8814  mapsnend  8984  isfinite2  9221  marypha1lem  9360  marypha2lem4  9365  infcllem  9415  en3lplem2  9542  cantnfp1  9610  carden2  9916  fseqenlem1  9953  iscard3  10022  cardnum  10023  alephinit  10024  cardinfima  10026  alephiso  10027  dfac10b  10069  dfackm  10096  isfin5-2  10320  brdom7disj  10460  brdom6disj  10461  fsuppmapnn0fiubex  13933  hash2prb  14413  hashle2prv  14419  hashtpg  14426  hash3tpb  14436  swrdnnn0nd  14597  wrd2ind  14664  cshwsexaOLD  14766  s4f1o  14860  cotr2g  14918  relexpindlem  15005  lcmfunsnlem2  16586  ncoprmlnprm  16674  vdwapun  16921  cshwsiun  17046  cshwshash  17051  grpss  18868  symgsubmefmnd  19312  pmtrfrn  19372  pmtrrn2  19374  pmtrprfvalrn  19402  issrg  20108  0ringnnzr  20445  acsfn1p  20719  unocv  21622  dsmmacl  21683  pmatcollpw2lem  22697  fvmptnn04if  22769  toptopon  22837  ordtbas2  23111  ordtrest2  23124  xmeterval  24353  isclmp  25030  ovolfcl  25400  eldv  25832  eltayl  26300  musumsum  27135  2sqreu  27400  2sqreunn  27401  2sqreult  27402  2sqreultb  27403  2sqreunnlt  27404  2sqreunnltb  27405  nosupinfsep  27677  umgrislfupgrlem  29102  numedglnl  29124  ausgrusgrb  29145  cplgr3v  29415  vtxd0nedgb  29469  finsumvtxdg2ssteplem1  29526  isrgr  29540  rgrusgrprc  29570  rgrprcx  29573  upgr2wlk  29647  dfpth2  29709  wwlksnwwlksnon  29895  usgr2wspthon  29945  isclwwlk  29963  clwwlkvbij  30092  iseupthf1o  30181  frcond2  30246  nfrgr2v  30251  4cycl2vnunb  30269  fusgr2wsp2nb  30313  frgrregord013  30374  lejdii  31517  mdslle1i  32296  mdslle2i  32297  mdslj1i  32298  mdslj2i  32299  mo5f  32468  n0nsnel  32494  unipreima  32617  2ndpreima  32681  mgccnv  32971  quslsm  33369  ordtrest2NEW  33906  ordtconnlem1  33907  ballotlem2  34473  plymulx0  34531  bnj115  34708  bnj156  34711  bnj206  34714  bnj110  34841  bnj121  34853  bnj124  34854  bnj130  34857  bnj153  34863  bnj207  34864  bnj581  34891  bnj611  34901  bnj864  34905  bnj865  34906  bnj893  34911  bnj1000  34924  bnj978  34932  bnj1040  34955  bnj1049  34957  bnj1133  34972  bnj1189  34992  satfv1  35343  satfvsucsuc  35345  satfdm  35349  satf0  35352  satf0op  35357  fmlafvel  35365  cnvco1  35739  cnvco2  35740  dfiota3  35904  ss-ax8  36206  trer  36297  nabi1i  36375  nabi2i  36376  bj-hbext  36691  bj-nnfbit  36733  bj-dvelimdv  36832  bj-gabima  36921  bj-elsngl  36949  bj-nuliotaALT  37039  bj-rest10  37069  bj-restuni  37078  con1bii2  37313  con2bii2  37314  topdifinfeq  37331  isbasisrelowllem2  37337  wl-1xor  37463  wl-1mintru1  37469  wl-sb8eut  37559  wl-sb8eutv  37560  inixp  37715  notbinot1  38066  notbinot2  38070  truconj  38088  sbccom2lem  38111  sbccom2  38112  sbccom2f  38113  tsim1  38117  tsxo3  38126  tsxo4  38127  trcoss2  38468  dfcomember3  38659  eqvreldmqs  38660  eqvreldmqs2  38661  dfmembpart2  38755  eldisjn0el  38791  isopos  39166  islvol5  39566  elpadd0  39796  dvhopellsm  41104  diblsmopel  41158  mapdvalc  41616  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  aks4d1p1p2  42051  aks4d1p7  42064  isprimroot  42074  aks6d1c1p1  42088  aks6d1c2p2  42100  sticksstones22  42149  unitscyglem4  42179  elpwbi  42211  redvmptabs  42341  dffltz  42615  rmxypairf1o  42893  onsupmaxb  43221  ifpnotnotb  43461  ifpdfxor  43469  ifpidg  43473  ifpim123g  43482  ifpim1g  43483  ifpimimb  43486  ifpimim  43491  rp-fakeanorass  43495  elmapintrab  43558  undmrnresiss  43586  clcnvlem  43605  sqrtcvallem1  43613  cnviun  43632  dfxor4  43748  dfhe3  43757  dffrege69  43914  dffrege76  43921  or3or  44005  uneqsn  44007  scottabf  44222  mnurndlem1  44263  ismnushort  44283  pm10.252  44343  pm10.253  44344  pm10.42  44346  aaanv  44370  pm13.195  44395  pm13.196a  44396  sbc3or  44515  en3lpVD  44827  3orbi123VD  44832  sbc3orgVD  44833  sbcoreleleqVD  44841  undif3VD  44864  ax6e2ndeqVD  44891  ax6e2ndeqALT  44913  sineq0ALT  44919  n0abso  44959  permaxsep  44990  permaxinf2lem  44995  uzwo4  45040  iindif2f  45147  allbutfiinf  45409  limsupequzmptlem  45719  cncfshift  45865  dvnmul  45934  dvnprodlem2  45938  rrxsnicc  46291  salexct  46325  sge00  46367  sge0iunmpt  46409  meadjiun  46457  carageneld  46493  ovncvrrp  46555  ovolval4lem1  46640  vonioo  46673  vonicc  46676  nsssmfmbf  46770  smfmullem4  46785  aibandbiaiffaiffb  46888  plcofph  46938  pldofph  46939  plvcofph  46940  plvcofphax  46941  plvofpos  46942  n0nsn2el  47019  fsetsniunop  47043  2reu8i  47107  aovov0bi  47190  tz6.12-afv2  47234  4an21  47264  ichbi12i  47454  ichnfimlem  47457  spr0nelg  47470  sprvalpwn0  47477  reuprpr  47517  requad2  47617  clnbgrel  47822  usgrexmpl2nb4  48019  pg4cyclnex  48110  copisnmnd  48150  pgrpgt2nabl  48347  lindslinindsimp2lem5  48444  islininds2  48466  ldepslinc  48491  line2ylem  48733