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  3159  r3ex  3168  r19.41  3233  rspc2gv  3587  ceqsrexbv  3611  rabeqcOLD  3646  2reu5lem1  3715  2reu5lem2  3716  2reu5lem3  3717  dfsbcq2  3745  cbvreucsf  3895  nss  4000  dfdif3OLD  4069  symdifass  4213  indifdi  4245  difab  4261  neq0  4303  un0  4345  in0  4346  ss0b  4352  eq0rdv  4358  2nreu  4395  ralidm  4463  ralf0  4465  reuprg  4655  snssb  4734  snssg  4735  ssunsn2  4778  iindif2  5026  eqsnuniex  5300  nssss  5398  snopeqop  5449  dffr6  5575  epse  5601  rnep  5869  mptpreima  6187  ralrnmpt  7030  fmptsng  7104  fmptsnd  7105  dff14a  7207  f13dfv  7211  weniso  7291  abnex  7693  uniuni  7698  frpoins3xp3g  8074  xpord3inddlem  8087  eroveu  8739  fsetexb  8791  mapsnend  8961  isfinite2  9187  marypha1lem  9323  marypha2lem4  9328  infcllem  9378  en3lplem2  9509  cantnfp1  9577  carden2  9883  fseqenlem1  9918  iscard3  9987  cardnum  9988  alephinit  9989  cardinfima  9991  alephiso  9992  dfac10b  10034  dfackm  10061  isfin5-2  10285  brdom7disj  10425  brdom6disj  10426  fsuppmapnn0fiubex  13899  hash2prb  14379  hashle2prv  14385  hashtpg  14392  hash3tpb  14402  swrdnnn0nd  14563  wrd2ind  14629  cshwsexaOLD  14731  s4f1o  14825  cotr2g  14883  relexpindlem  14970  lcmfunsnlem2  16551  ncoprmlnprm  16639  vdwapun  16886  cshwsiun  17011  cshwshash  17016  grpss  18833  symgsubmefmnd  19277  pmtrfrn  19337  pmtrrn2  19339  pmtrprfvalrn  19367  issrg  20073  0ringnnzr  20410  acsfn1p  20684  unocv  21587  dsmmacl  21648  pmatcollpw2lem  22662  fvmptnn04if  22734  toptopon  22802  ordtbas2  23076  ordtrest2  23089  xmeterval  24318  isclmp  24995  ovolfcl  25365  eldv  25797  eltayl  26265  musumsum  27100  2sqreu  27365  2sqreunn  27366  2sqreult  27367  2sqreultb  27368  2sqreunnlt  27369  2sqreunnltb  27370  nosupinfsep  27642  umgrislfupgrlem  29071  numedglnl  29093  ausgrusgrb  29114  cplgr3v  29384  vtxd0nedgb  29438  finsumvtxdg2ssteplem1  29495  isrgr  29509  rgrusgrprc  29539  rgrprcx  29542  upgr2wlk  29616  dfpth2  29678  wwlksnwwlksnon  29864  usgr2wspthon  29914  isclwwlk  29932  clwwlkvbij  30061  iseupthf1o  30150  frcond2  30215  nfrgr2v  30220  4cycl2vnunb  30238  fusgr2wsp2nb  30282  frgrregord013  30343  lejdii  31486  mdslle1i  32265  mdslle2i  32266  mdslj1i  32267  mdslj2i  32268  mo5f  32437  n0nsnel  32464  unipreima  32594  2ndpreima  32658  mgccnv  32950  quslsm  33351  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  35356  satfvsucsuc  35358  satfdm  35362  satf0  35365  satf0op  35370  fmlafvel  35378  cnvco1  35752  cnvco2  35753  dfiota3  35917  ss-ax8  36219  trer  36310  nabi1i  36388  nabi2i  36389  bj-hbext  36704  bj-nnfbit  36746  bj-dvelimdv  36845  bj-gabima  36934  bj-elsngl  36962  bj-nuliotaALT  37052  bj-rest10  37082  bj-restuni  37091  con1bii2  37326  con2bii2  37327  topdifinfeq  37344  isbasisrelowllem2  37350  wl-1xor  37476  wl-1mintru1  37482  wl-sb8eut  37572  wl-sb8eutv  37573  inixp  37728  notbinot1  38079  notbinot2  38083  truconj  38101  sbccom2lem  38124  sbccom2  38125  sbccom2f  38126  tsim1  38130  tsxo3  38139  tsxo4  38140  trcoss2  38481  dfcomember3  38672  eqvreldmqs  38673  eqvreldmqs2  38674  dfmembpart2  38768  eldisjn0el  38804  isopos  39179  islvol5  39578  elpadd0  39808  dvhopellsm  41116  diblsmopel  41170  mapdvalc  41628  3factsumint2  42015  3factsumint3  42016  3factsumint4  42017  aks4d1p1p2  42063  aks4d1p7  42076  isprimroot  42086  aks6d1c1p1  42100  aks6d1c2p2  42112  sticksstones22  42161  unitscyglem4  42191  elpwbi  42223  redvmptabs  42353  dffltz  42627  rmxypairf1o  42904  onsupmaxb  43232  ifpnotnotb  43472  ifpdfxor  43480  ifpidg  43484  ifpim123g  43493  ifpim1g  43494  ifpimimb  43497  ifpimim  43502  rp-fakeanorass  43506  elmapintrab  43569  undmrnresiss  43597  clcnvlem  43616  sqrtcvallem1  43624  cnviun  43643  dfxor4  43759  dfhe3  43768  dffrege69  43925  dffrege76  43932  or3or  44016  uneqsn  44018  scottabf  44233  mnurndlem1  44274  ismnushort  44294  pm10.252  44354  pm10.253  44355  pm10.42  44357  aaanv  44381  pm13.195  44406  pm13.196a  44407  sbc3or  44526  en3lpVD  44838  3orbi123VD  44843  sbc3orgVD  44844  sbcoreleleqVD  44852  undif3VD  44875  ax6e2ndeqVD  44902  ax6e2ndeqALT  44924  sineq0ALT  44930  n0abso  44970  permaxsep  45001  permaxinf2lem  45006  uzwo4  45051  iindif2f  45158  allbutfiinf  45419  limsupequzmptlem  45729  cncfshift  45875  dvnmul  45944  dvnprodlem2  45948  rrxsnicc  46301  salexct  46335  sge00  46377  sge0iunmpt  46419  meadjiun  46467  carageneld  46503  ovncvrrp  46565  ovolval4lem1  46650  vonioo  46683  vonicc  46686  nsssmfmbf  46780  smfmullem4  46795  aibandbiaiffaiffb  46898  plcofph  46948  pldofph  46949  plvcofph  46950  plvcofphax  46951  plvofpos  46952  n0nsn2el  47029  fsetsniunop  47053  2reu8i  47117  aovov0bi  47200  tz6.12-afv2  47244  4an21  47274  ichbi12i  47464  ichnfimlem  47467  spr0nelg  47480  sprvalpwn0  47487  reuprpr  47527  requad2  47627  clnbgrel  47832  usgrexmpl2nb4  48039  pg4cyclnex  48131  copisnmnd  48173  pgrpgt2nabl  48370  lindslinindsimp2lem5  48467  islininds2  48489  ldepslinc  48514  line2ylem  48756