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  5881  mptpreima  6200  ralrnmpt  7051  fmptsng  7125  fmptsnd  7126  dff14a  7228  f13dfv  7232  weniso  7312  abnex  7714  uniuni  7719  frpoins3xp3g  8098  xpord3inddlem  8111  eroveu  8763  fsetexb  8815  mapsnend  8985  isfinite2  9222  marypha1lem  9361  marypha2lem4  9366  infcllem  9416  en3lplem2  9545  cantnfp1  9613  carden2  9919  fseqenlem1  9956  iscard3  10025  cardnum  10026  alephinit  10027  cardinfima  10029  alephiso  10030  dfac10b  10072  dfackm  10099  isfin5-2  10323  brdom7disj  10463  brdom6disj  10464  fsuppmapnn0fiubex  13936  hash2prb  14416  hashle2prv  14422  hashtpg  14429  hash3tpb  14439  swrdnnn0nd  14600  wrd2ind  14666  cshwsexaOLD  14768  s4f1o  14862  cotr2g  14920  relexpindlem  15007  lcmfunsnlem2  16588  ncoprmlnprm  16676  vdwapun  16923  cshwsiun  17048  cshwshash  17053  grpss  18870  symgsubmefmnd  19314  pmtrfrn  19374  pmtrrn2  19376  pmtrprfvalrn  19404  issrg  20110  0ringnnzr  20447  acsfn1p  20721  unocv  21624  dsmmacl  21685  pmatcollpw2lem  22699  fvmptnn04if  22771  toptopon  22839  ordtbas2  23113  ordtrest2  23126  xmeterval  24355  isclmp  25032  ovolfcl  25402  eldv  25834  eltayl  26302  musumsum  27137  2sqreu  27402  2sqreunn  27403  2sqreult  27404  2sqreultb  27405  2sqreunnlt  27406  2sqreunnltb  27407  nosupinfsep  27679  umgrislfupgrlem  29104  numedglnl  29126  ausgrusgrb  29147  cplgr3v  29417  vtxd0nedgb  29471  finsumvtxdg2ssteplem1  29528  isrgr  29542  rgrusgrprc  29572  rgrprcx  29575  upgr2wlk  29649  dfpth2  29711  wwlksnwwlksnon  29897  usgr2wspthon  29947  isclwwlk  29965  clwwlkvbij  30094  iseupthf1o  30183  frcond2  30248  nfrgr2v  30253  4cycl2vnunb  30271  fusgr2wsp2nb  30315  frgrregord013  30376  lejdii  31519  mdslle1i  32298  mdslle2i  32299  mdslj1i  32300  mdslj2i  32301  mo5f  32470  n0nsnel  32496  unipreima  32619  2ndpreima  32683  mgccnv  32973  quslsm  33371  ordtrest2NEW  33908  ordtconnlem1  33909  ballotlem2  34475  plymulx0  34533  bnj115  34710  bnj156  34713  bnj206  34716  bnj110  34843  bnj121  34855  bnj124  34856  bnj130  34859  bnj153  34865  bnj207  34866  bnj581  34893  bnj611  34903  bnj864  34907  bnj865  34908  bnj893  34913  bnj1000  34926  bnj978  34934  bnj1040  34957  bnj1049  34959  bnj1133  34974  bnj1189  34994  satfv1  35345  satfvsucsuc  35347  satfdm  35351  satf0  35354  satf0op  35359  fmlafvel  35367  cnvco1  35741  cnvco2  35742  dfiota3  35906  ss-ax8  36208  trer  36299  nabi1i  36377  nabi2i  36378  bj-hbext  36693  bj-nnfbit  36735  bj-dvelimdv  36834  bj-gabima  36923  bj-elsngl  36951  bj-nuliotaALT  37041  bj-rest10  37071  bj-restuni  37080  con1bii2  37315  con2bii2  37316  topdifinfeq  37333  isbasisrelowllem2  37339  wl-1xor  37465  wl-1mintru1  37471  wl-sb8eut  37561  wl-sb8eutv  37562  inixp  37717  notbinot1  38068  notbinot2  38072  truconj  38090  sbccom2lem  38113  sbccom2  38114  sbccom2f  38115  tsim1  38119  tsxo3  38128  tsxo4  38129  trcoss2  38470  dfcomember3  38661  eqvreldmqs  38662  eqvreldmqs2  38663  dfmembpart2  38757  eldisjn0el  38793  isopos  39168  islvol5  39568  elpadd0  39798  dvhopellsm  41106  diblsmopel  41160  mapdvalc  41618  3factsumint2  42005  3factsumint3  42006  3factsumint4  42007  aks4d1p1p2  42053  aks4d1p7  42066  isprimroot  42076  aks6d1c1p1  42090  aks6d1c2p2  42102  sticksstones22  42151  unitscyglem4  42181  elpwbi  42213  redvmptabs  42343  dffltz  42617  rmxypairf1o  42895  onsupmaxb  43223  ifpnotnotb  43463  ifpdfxor  43471  ifpidg  43475  ifpim123g  43484  ifpim1g  43485  ifpimimb  43488  ifpimim  43493  rp-fakeanorass  43497  elmapintrab  43560  undmrnresiss  43588  clcnvlem  43607  sqrtcvallem1  43615  cnviun  43634  dfxor4  43750  dfhe3  43759  dffrege69  43916  dffrege76  43923  or3or  44007  uneqsn  44009  scottabf  44224  mnurndlem1  44265  ismnushort  44285  pm10.252  44345  pm10.253  44346  pm10.42  44348  aaanv  44372  pm13.195  44397  pm13.196a  44398  sbc3or  44517  en3lpVD  44829  3orbi123VD  44834  sbc3orgVD  44835  sbcoreleleqVD  44843  undif3VD  44866  ax6e2ndeqVD  44893  ax6e2ndeqALT  44915  sineq0ALT  44921  n0abso  44961  permaxsep  44992  permaxinf2lem  44997  uzwo4  45042  iindif2f  45149  allbutfiinf  45411  limsupequzmptlem  45721  cncfshift  45867  dvnmul  45936  dvnprodlem2  45940  rrxsnicc  46293  salexct  46327  sge00  46369  sge0iunmpt  46411  meadjiun  46459  carageneld  46495  ovncvrrp  46557  ovolval4lem1  46642  vonioo  46675  vonicc  46678  nsssmfmbf  46772  smfmullem4  46787  aibandbiaiffaiffb  46890  plcofph  46940  pldofph  46941  plvcofph  46942  plvcofphax  46943  plvofpos  46944  n0nsn2el  47021  fsetsniunop  47045  2reu8i  47109  aovov0bi  47192  tz6.12-afv2  47236  4an21  47266  ichbi12i  47456  ichnfimlem  47459  spr0nelg  47472  sprvalpwn0  47479  reuprpr  47519  requad2  47619  clnbgrel  47824  usgrexmpl2nb4  48021  pg4cyclnex  48112  copisnmnd  48152  pgrpgt2nabl  48349  lindslinindsimp2lem5  48446  islininds2  48468  ldepslinc  48493  line2ylem  48735