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  356  nbn  372  xor3  382  pm5.41  390  pm4.63  397  pm4.61  404  pm4.76  518  anidm  564  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  1497  nornot  1531  truan  1551  truimfal  1564  nottru  1567  falbitru  1570  nic-dfim  1670  nic-dfneg  1671  2nalexn  1829  2nexaln  1831  equvinv  2031  cleljust  2114  sbelx  2244  sb5OLD  2267  sb6rfv  2352  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  3231  ralcom4OLD  3283  rspc2gv  3621  ceqsrexbv  3644  clel4OLD  3654  rabeqcOLD  3681  2reu5lem1  3751  2reu5lem2  3752  2reu5lem3  3753  dfsbcq2  3780  cbvreucsf  3940  nss  4046  ss2abdv  4060  dfdif3  4114  symdifass  4251  indifdi  4283  difab  4300  neq0  4345  ab0OLD  4375  un0  4390  in0  4391  ss0b  4397  eq0rdv  4404  2nreu  4441  ralidm  4511  ralf0  4513  rexdifpr  4661  reuprg  4707  snssb  4786  snssg  4787  ssunsn2  4830  iindif2  5080  eqsnuniex  5359  nssss  5455  snopeqop  5506  dffr6  5634  epse  5659  rnep  5926  cotrgOLDOLD  6110  mptpreima  6237  ralrnmpt  7097  fmptsng  7168  fmptsnd  7169  dff14a  7272  f13dfv  7275  weniso  7354  abnex  7748  uniuni  7753  frpoins3xp3g  8132  xpord3inddlem  8145  eroveu  8812  fsetexb  8864  mapsnend  9042  isfinite2  9307  marypha1lem  9434  marypha2lem4  9439  infcllem  9488  en3lplem2  9614  cantnfp1  9682  carden2  9988  fseqenlem1  10025  iscard3  10094  cardnum  10095  alephinit  10096  cardinfima  10098  alephiso  10099  dfac10b  10140  dfackm  10167  isfin5-2  10392  brdom7disj  10532  brdom6disj  10533  fsuppmapnn0fiubex  13964  hash2prb  14440  hashle2prv  14446  hashtpg  14453  swrdnnn0nd  14613  wrd2ind  14680  cshwsexaOLD  14782  s4f1o  14876  cotr2g  14930  relexpindlem  15017  lcmfunsnlem2  16584  ncoprmlnprm  16671  vdwapun  16914  cshwsiun  17040  cshwshash  17045  grpss  18882  symgsubmefmnd  19314  pmtrfrn  19374  pmtrrn2  19376  pmtrprfvalrn  19404  issrg  20089  0ringnnzr  20421  acsfn1p  20646  df2idl2  21097  unocv  21542  dsmmacl  21605  pmatcollpw2lem  22598  fvmptnn04if  22670  toptopon  22738  ordtbas2  23014  ordtrest2  23027  xmeterval  24257  isclmp  24943  ovolfcl  25314  eldv  25746  eltayl  26210  musumsum  27036  2sqreu  27301  2sqreunn  27302  2sqreult  27303  2sqreultb  27304  2sqreunnlt  27305  2sqreunnltb  27306  nosupinfsep  27577  umgrislfupgrlem  28814  numedglnl  28836  ausgrusgrb  28857  cplgr3v  29124  vtxd0nedgb  29177  finsumvtxdg2ssteplem1  29234  isrgr  29248  rgrusgrprc  29278  rgrprcx  29281  upgr2wlk  29357  wwlksnwwlksnon  29601  usgr2wspthon  29651  isclwwlk  29669  clwwlkvbij  29798  iseupthf1o  29887  frcond2  29952  nfrgr2v  29957  4cycl2vnunb  29975  fusgr2wsp2nb  30019  frgrregord013  30080  lejdii  31223  mdslle1i  32002  mdslle2i  32003  mdslj1i  32004  mdslj2i  32005  mo5f  32161  unipreima  32301  2ndpreima  32361  mgccnv  32601  quslsm  32955  ordtrest2NEW  33366  ordtconnlem1  33367  ballotlem2  33950  plymulx0  34021  bnj115  34199  bnj156  34202  bnj206  34205  bnj110  34332  bnj121  34344  bnj124  34345  bnj130  34348  bnj153  34354  bnj207  34355  bnj581  34382  bnj611  34392  bnj864  34396  bnj865  34397  bnj893  34402  bnj1000  34415  bnj978  34423  bnj1040  34446  bnj1049  34448  bnj1133  34463  bnj1189  34483  satfv1  34817  satfvsucsuc  34819  satfdm  34823  satf0  34826  satf0op  34831  fmlafvel  34839  cnvco1  35198  cnvco2  35199  dfiota3  35364  trer  35664  nabi1i  35742  nabi2i  35743  bj-hbext  36051  bj-nnfbit  36093  bj-dvelimdv  36193  bj-gabima  36283  bj-elsngl  36312  bj-nuliotaALT  36402  bj-rest10  36432  bj-restuni  36441  con1bii2  36676  con2bii2  36677  topdifinfeq  36694  isbasisrelowllem2  36700  wl-1xor  36826  wl-1mintru1  36832  wl-sb8eut  36905  inixp  37059  notbinot1  37410  notbinot2  37414  truconj  37432  sbccom2lem  37455  sbccom2  37456  sbccom2f  37457  tsim1  37461  tsxo3  37470  tsxo4  37471  trcoss2  37817  dfcomember3  38007  eqvreldmqs  38008  eqvreldmqs2  38009  dfmembpart2  38103  eldisjn0el  38139  isopos  38513  islvol5  38913  elpadd0  39143  dvhopellsm  40451  diblsmopel  40505  mapdvalc  40963  3factsumint2  41353  3factsumint3  41354  3factsumint4  41355  aks4d1p1p2  41401  aks4d1p7  41414  aks6d1c2p2  41423  sticksstones22  41450  elpwbi  41515  dffltz  41838  rmxypairf1o  42112  onsupmaxb  42450  ifpnotnotb  42692  ifpdfxor  42700  ifpidg  42704  ifpim123g  42713  ifpim1g  42714  ifpimimb  42717  ifpimim  42722  rp-fakeanorass  42726  elmapintrab  42789  undmrnresiss  42817  clcnvlem  42836  sqrtcvallem1  42844  cnviun  42863  dfxor4  42979  dfhe3  42988  dffrege69  43145  dffrege76  43152  or3or  43236  uneqsn  43238  scottabf  43461  mnurndlem1  43502  ismnushort  43522  pm10.252  43582  pm10.253  43583  pm10.42  43585  aaanv  43609  pm13.195  43634  pm13.196a  43635  sbc3or  43755  en3lpVD  44068  3orbi123VD  44073  sbc3orgVD  44074  sbcoreleleqVD  44082  undif3VD  44105  ax6e2ndeqVD  44132  ax6e2ndeqALT  44154  sineq0ALT  44160  uzwo4  44201  iindif2f  44315  allbutfiinf  44588  limsupequzmptlem  44902  cncfshift  45048  dvnmul  45117  dvnprodlem2  45121  rrxsnicc  45474  salexct  45508  sge00  45550  sge0iunmpt  45592  meadjiun  45640  carageneld  45676  ovncvrrp  45738  ovolval4lem1  45823  vonioo  45856  vonicc  45859  nsssmfmbf  45953  smfmullem4  45968  aibandbiaiffaiffb  46062  plcofph  46112  pldofph  46113  plvcofph  46114  plvcofphax  46115  plvofpos  46116  n0nsn2el  46193  fsetsniunop  46217  2reu8i  46279  aovov0bi  46362  tz6.12-afv2  46406  4an21  46436  ichbi12i  46586  ichnfimlem  46589  spr0nelg  46602  sprvalpwn0  46609  reuprpr  46649  requad2  46749  copisnmnd  47005  pgrpgt2nabl  47204  lindslinindsimp2lem5  47304  islininds2  47326  ldepslinc  47351  line2ylem  47598