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  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  398  pm4.61  405  pm4.76  519  anidm  565  an21  641  an43  655  anabs1  659  anabs7  661  pm4.87  840  pm4.64  846  pm4.25  903  pm4.77  960  pm4.53  983  pm4.55  985  pm4.56  986  pm4.57  988  pm5.63  1017  3anor  1107  3oran  1108  syl3anbr  1161  3an6  1445  nanbi  1495  nornot  1529  truan  1550  truimfal  1563  nottru  1566  falbitru  1569  falnorfalOLD  1593  nic-dfim  1672  nic-dfneg  1673  2nalexn  1831  2nexaln  1833  equvinv  2033  cleljust  2116  sbelx  2247  sb5OLD  2270  sb6rfv  2356  cleljustALT  2363  cleljustALT2  2364  dvelimf  2449  sb5rf  2468  sb6rf  2469  sb10f  2533  nexmo  2542  exists2  2664  cleljustab  2719  abeq1i  2877  abbi2dv  2878  nfabdwOLD  2932  nne  2948  necon3bbii  2992  necon2abii  2995  necon2bbii  2996  nnel  3059  ralcom4OLD  3166  nelbOLD  3197  rspc2gv  3570  ceqsrexbv  3587  clel4OLD  3596  rabeqc  3623  2reu5lem1  3691  2reu5lem2  3692  2reu5lem3  3693  dfsbcq2  3720  cbvreucsf  3880  nss  3984  ss2abdv  3998  dfdif3  4050  symdifass  4186  indifdi  4218  difab  4235  neq0  4280  ab0OLD  4310  un0  4325  in0  4326  ss0b  4332  eq0rdv  4339  2nreu  4376  ralidm  4443  ralf0  4445  rexdifpr  4595  reuprg  4640  ssunsn2  4761  iindif2  5007  eqsnuniex  5284  nssss  5372  snopeqop  5421  dffr6  5548  epse  5573  rnep  5839  cotrgOLD  6021  mptpreima  6146  ralrnmpt  6981  fmptsng  7049  fmptsnd  7050  dff14a  7152  f13dfv  7155  weniso  7234  abnex  7616  uniuni  7621  suppvalbr  7990  eroveu  8610  fsetexb  8661  mapsnend  8835  isfinite2  9081  marypha1lem  9201  marypha2lem4  9206  infcllem  9255  en3lplem2  9380  cantnfp1  9448  carden2  9754  fseqenlem1  9789  iscard3  9858  cardnum  9859  alephinit  9860  cardinfima  9862  alephiso  9863  dfac10b  9904  dfackm  9931  isfin5-2  10156  brdom7disj  10296  brdom6disj  10297  fsuppmapnn0fiubex  13721  hash2prb  14195  hashle2prv  14201  hashtpg  14208  swrdnnn0nd  14378  wrd2ind  14445  cshwsexa  14546  s4f1o  14640  cotr2g  14696  relexpindlem  14783  lcmfunsnlem2  16354  ncoprmlnprm  16441  vdwapun  16684  cshwsiun  16810  cshwshash  16815  grpss  18606  symgsubmefmnd  19015  pmtrfrn  19075  pmtrrn2  19077  pmtrprfvalrn  19105  issrg  19752  acsfn1p  20076  0ringnnzr  20549  unocv  20894  dsmmacl  20957  pmatcollpw2lem  21935  fvmptnn04if  22007  toptopon  22075  ordtbas2  22351  ordtrest2  22364  xmeterval  23594  isclmp  24269  ovolfcl  24639  eldv  25071  eltayl  25528  musumsum  26350  2sqreu  26613  2sqreunn  26614  2sqreult  26615  2sqreultb  26616  2sqreunnlt  26617  2sqreunnltb  26618  umgrislfupgrlem  27501  numedglnl  27523  ausgrusgrb  27544  cplgr3v  27811  vtxd0nedgb  27864  finsumvtxdg2ssteplem1  27921  isrgr  27935  rgrusgrprc  27965  rgrprcx  27968  upgr2wlk  28045  wwlksnwwlksnon  28289  usgr2wspthon  28339  isclwwlk  28357  clwwlkvbij  28486  iseupthf1o  28575  frcond2  28640  nfrgr2v  28645  4cycl2vnunb  28663  fusgr2wsp2nb  28707  frgrregord013  28768  lejdii  29909  mdslle1i  30688  mdslle2i  30689  mdslj1i  30690  mdslj2i  30691  mo5f  30846  unipreima  30990  2ndpreima  31049  mgccnv  31286  quslsm  31602  ordtrest2NEW  31882  ordtconnlem1  31883  ballotlem2  32464  plymulx0  32535  bnj115  32713  bnj156  32716  bnj206  32719  bnj110  32847  bnj121  32859  bnj124  32860  bnj130  32863  bnj153  32869  bnj207  32870  bnj581  32897  bnj611  32907  bnj864  32911  bnj865  32912  bnj893  32917  bnj1000  32930  bnj978  32938  bnj1040  32961  bnj1049  32963  bnj1133  32978  bnj1189  32998  satfv1  33334  satfvsucsuc  33336  satfdm  33340  satf0  33343  satf0op  33348  fmlafvel  33356  cnvco1  33735  cnvco2  33736  nosupinfsep  33944  dfiota3  34234  trer  34514  nabi1i  34592  nabi2i  34593  bj-hbext  34901  bj-nnfbit  34943  bj-dvelimdv  35044  bj-gabima  35137  bj-elsngl  35167  bj-nuliotaALT  35238  bj-rest10  35268  bj-restuni  35277  con1bii2  35512  con2bii2  35513  topdifinfeq  35530  isbasisrelowllem2  35536  wl-1xor  35662  wl-1mintru1  35668  wl-sb8eut  35741  inixp  35895  notbinot1  36246  notbinot2  36250  truconj  36268  sbccom2lem  36291  sbccom2  36292  sbccom2f  36293  tsim1  36297  tsxo3  36306  tsxo4  36307  trcoss2  36609  dfmember3  36793  eqvreldmqs  36794  isopos  37201  islvol5  37600  elpadd0  37830  dvhopellsm  39138  diblsmopel  39192  mapdvalc  39650  3factsumint2  40037  3factsumint3  40038  3factsumint4  40039  aks4d1p1p2  40085  aks4d1p7  40098  sticksstones22  40131  elpwbi  40212  dffltz  40478  rmxypairf1o  40740  ifpnotnotb  41093  ifpdfxor  41101  ifpidg  41105  ifpim123g  41114  ifpim1g  41115  ifpimimb  41118  ifpimim  41123  rp-fakeanorass  41127  elmapintrab  41191  undmrnresiss  41219  clcnvlem  41238  sqrtcvallem1  41246  cnviun  41265  dfxor4  41381  dfhe3  41390  dffrege69  41547  dffrege76  41554  or3or  41638  uneqsn  41640  scottabf  41865  mnurndlem1  41906  ismnushort  41926  pm10.252  41986  pm10.253  41987  pm10.42  41989  aaanv  42013  pm13.195  42038  pm13.196a  42039  sbc3or  42159  en3lpVD  42472  3orbi123VD  42477  sbc3orgVD  42478  sbcoreleleqVD  42486  undif3VD  42509  ax6e2ndeqVD  42536  ax6e2ndeqALT  42558  sineq0ALT  42564  uzwo4  42608  fompt  42737  allbutfiinf  42967  limsupequzmptlem  43276  cncfshift  43422  dvnmul  43491  dvnprodlem2  43495  rrxsnicc  43848  salexct  43880  sge00  43921  sge0iunmpt  43963  meadjiun  44011  carageneld  44047  ovncvrrp  44109  ovolval4lem1  44194  vonioo  44227  vonicc  44230  nsssmfmbf  44324  smfmullem4  44339  aibandbiaiffaiffb  44400  plcofph  44450  pldofph  44451  plvcofph  44452  plvcofphax  44453  plvofpos  44454  fsetsniunop  44554  2reu8i  44616  aovov0bi  44699  tz6.12-afv2  44743  4an21  44773  ichbi12i  44923  ichnfimlem  44926  spr0nelg  44939  sprvalpwn0  44946  reuprpr  44986  requad2  45086  copisnmnd  45374  pgrpgt2nabl  45713  lindslinindsimp2lem5  45814  islininds2  45836  ldepslinc  45861  line2ylem  46108