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  276  bitr3i  277  bitr4i  278  bitr3id  285  bitr3di  286  bitr4di  289  bitr4id  290  mtbir  323  sylnibr  329  sylnbir  331  xchnxbir  333  xchbinxr  335  con1bii  357  nbn  373  xor3  384  pm5.41  392  pm4.63  399  pm4.61  406  pm4.76  520  anidm  566  an21  643  an43  657  anabs1  661  anabs7  663  pm4.87  842  pm4.64  848  pm4.25  905  pm4.77  962  pm4.53  985  pm4.55  987  pm4.56  988  pm4.57  990  pm5.63  1019  3anor  1109  3oran  1110  syl3anbr  1163  3an6  1447  nanbi  1499  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1672  nic-dfneg  1673  2nalexn  1831  2nexaln  1833  equvinv  2033  cleljust  2116  sbelx  2246  sb5OLD  2269  sb6rfv  2354  cleljustALT  2362  cleljustALT2  2363  dvelimf  2448  sb5rf  2467  sb6rf  2468  sb10f  2527  nexmo  2536  exists2  2658  cleljustab  2713  eqabdv  2868  eqabcri  2879  nfabdwOLD  2928  nne  2945  necon3bbii  2989  necon2abii  2992  necon2bbii  2993  nnel  3057  nelbOLD  3233  ralcom4OLD  3285  rspc2gv  3622  ceqsrexbv  3645  clel4OLD  3655  rabeqcOLD  3682  2reu5lem1  3752  2reu5lem2  3753  2reu5lem3  3754  dfsbcq2  3781  cbvreucsf  3941  nss  4047  ss2abdv  4061  dfdif3  4115  symdifass  4252  indifdi  4284  difab  4301  neq0  4346  ab0OLD  4376  un0  4391  in0  4392  ss0b  4398  eq0rdv  4405  2nreu  4442  ralidm  4512  ralf0  4514  rexdifpr  4662  reuprg  4708  snssb  4787  snssg  4788  ssunsn2  4831  iindif2  5081  eqsnuniex  5360  nssss  5456  snopeqop  5507  dffr6  5635  epse  5660  rnep  5927  cotrgOLDOLD  6111  mptpreima  6238  ralrnmpt  7098  fmptsng  7166  fmptsnd  7167  dff14a  7269  f13dfv  7272  weniso  7351  abnex  7744  uniuni  7749  frpoins3xp3g  8127  xpord3inddlem  8140  eroveu  8806  fsetexb  8858  mapsnend  9036  isfinite2  9301  marypha1lem  9428  marypha2lem4  9433  infcllem  9482  en3lplem2  9608  cantnfp1  9676  carden2  9982  fseqenlem1  10019  iscard3  10088  cardnum  10089  alephinit  10090  cardinfima  10092  alephiso  10093  dfac10b  10134  dfackm  10161  isfin5-2  10386  brdom7disj  10526  brdom6disj  10527  fsuppmapnn0fiubex  13957  hash2prb  14433  hashle2prv  14439  hashtpg  14446  swrdnnn0nd  14606  wrd2ind  14673  cshwsexaOLD  14775  s4f1o  14869  cotr2g  14923  relexpindlem  15010  lcmfunsnlem2  16577  ncoprmlnprm  16664  vdwapun  16907  cshwsiun  17033  cshwshash  17038  grpss  18840  symgsubmefmnd  19266  pmtrfrn  19326  pmtrrn2  19328  pmtrprfvalrn  19356  issrg  20011  0ringnnzr  20302  acsfn1p  20415  df2idl2  20860  unocv  21233  dsmmacl  21296  pmatcollpw2lem  22279  fvmptnn04if  22351  toptopon  22419  ordtbas2  22695  ordtrest2  22708  xmeterval  23938  isclmp  24613  ovolfcl  24983  eldv  25415  eltayl  25872  musumsum  26696  2sqreu  26959  2sqreunn  26960  2sqreult  26961  2sqreultb  26962  2sqreunnlt  26963  2sqreunnltb  26964  nosupinfsep  27235  umgrislfupgrlem  28382  numedglnl  28404  ausgrusgrb  28425  cplgr3v  28692  vtxd0nedgb  28745  finsumvtxdg2ssteplem1  28802  isrgr  28816  rgrusgrprc  28846  rgrprcx  28849  upgr2wlk  28925  wwlksnwwlksnon  29169  usgr2wspthon  29219  isclwwlk  29237  clwwlkvbij  29366  iseupthf1o  29455  frcond2  29520  nfrgr2v  29525  4cycl2vnunb  29543  fusgr2wsp2nb  29587  frgrregord013  29648  lejdii  30791  mdslle1i  31570  mdslle2i  31571  mdslj1i  31572  mdslj2i  31573  mo5f  31729  unipreima  31869  2ndpreima  31929  mgccnv  32169  quslsm  32516  ordtrest2NEW  32903  ordtconnlem1  32904  ballotlem2  33487  plymulx0  33558  bnj115  33736  bnj156  33739  bnj206  33742  bnj110  33869  bnj121  33881  bnj124  33882  bnj130  33885  bnj153  33891  bnj207  33892  bnj581  33919  bnj611  33929  bnj864  33933  bnj865  33934  bnj893  33939  bnj1000  33952  bnj978  33960  bnj1040  33983  bnj1049  33985  bnj1133  34000  bnj1189  34020  satfv1  34354  satfvsucsuc  34356  satfdm  34360  satf0  34363  satf0op  34368  fmlafvel  34376  cnvco1  34729  cnvco2  34730  dfiota3  34895  trer  35201  nabi1i  35279  nabi2i  35280  bj-hbext  35588  bj-nnfbit  35630  bj-dvelimdv  35730  bj-gabima  35820  bj-elsngl  35849  bj-nuliotaALT  35939  bj-rest10  35969  bj-restuni  35978  con1bii2  36213  con2bii2  36214  topdifinfeq  36231  isbasisrelowllem2  36237  wl-1xor  36363  wl-1mintru1  36369  wl-sb8eut  36442  inixp  36596  notbinot1  36947  notbinot2  36951  truconj  36969  sbccom2lem  36992  sbccom2  36993  sbccom2f  36994  tsim1  36998  tsxo3  37007  tsxo4  37008  trcoss2  37354  dfcomember3  37544  eqvreldmqs  37545  eqvreldmqs2  37546  dfmembpart2  37640  eldisjn0el  37676  isopos  38050  islvol5  38450  elpadd0  38680  dvhopellsm  39988  diblsmopel  40042  mapdvalc  40500  3factsumint2  40887  3factsumint3  40888  3factsumint4  40889  aks4d1p1p2  40935  aks4d1p7  40948  aks6d1c2p2  40957  sticksstones22  40984  elpwbi  41049  dffltz  41376  rmxypairf1o  41650  onsupmaxb  41988  ifpnotnotb  42230  ifpdfxor  42238  ifpidg  42242  ifpim123g  42251  ifpim1g  42252  ifpimimb  42255  ifpimim  42260  rp-fakeanorass  42264  elmapintrab  42327  undmrnresiss  42355  clcnvlem  42374  sqrtcvallem1  42382  cnviun  42401  dfxor4  42517  dfhe3  42526  dffrege69  42683  dffrege76  42690  or3or  42774  uneqsn  42776  scottabf  42999  mnurndlem1  43040  ismnushort  43060  pm10.252  43120  pm10.253  43121  pm10.42  43123  aaanv  43147  pm13.195  43172  pm13.196a  43173  sbc3or  43293  en3lpVD  43606  3orbi123VD  43611  sbc3orgVD  43612  sbcoreleleqVD  43620  undif3VD  43643  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  sineq0ALT  43698  uzwo4  43740  iindif2f  43854  fompt  43890  allbutfiinf  44130  limsupequzmptlem  44444  cncfshift  44590  dvnmul  44659  dvnprodlem2  44663  rrxsnicc  45016  salexct  45050  sge00  45092  sge0iunmpt  45134  meadjiun  45182  carageneld  45218  ovncvrrp  45280  ovolval4lem1  45365  vonioo  45398  vonicc  45401  nsssmfmbf  45495  smfmullem4  45510  aibandbiaiffaiffb  45604  plcofph  45654  pldofph  45655  plvcofph  45656  plvcofphax  45657  plvofpos  45658  n0nsn2el  45735  fsetsniunop  45759  2reu8i  45821  aovov0bi  45904  tz6.12-afv2  45948  4an21  45978  ichbi12i  46128  ichnfimlem  46131  spr0nelg  46144  sprvalpwn0  46151  reuprpr  46191  requad2  46291  copisnmnd  46579  pgrpgt2nabl  47042  lindslinindsimp2lem5  47143  islininds2  47165  ldepslinc  47190  line2ylem  47437