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  3167  r3ex  3176  r19.41  3241  rspc2gv  3598  ceqsrexbv  3622  rabeqcOLD  3657  2reu5lem1  3726  2reu5lem2  3727  2reu5lem3  3728  dfsbcq2  3756  cbvreucsf  3906  nss  4011  dfdif3OLD  4081  symdifass  4225  indifdi  4257  difab  4273  neq0  4315  un0  4357  in0  4358  ss0b  4364  eq0rdv  4370  2nreu  4407  ralidm  4475  ralf0  4477  reuprg  4667  snssb  4746  snssg  4747  ssunsn2  4791  iindif2  5041  eqsnuniex  5316  nssss  5415  snopeqop  5466  dffr6  5594  epse  5620  rnep  5890  cotrgOLDOLD  6082  mptpreima  6211  ralrnmpt  7068  fmptsng  7142  fmptsnd  7143  dff14a  7245  f13dfv  7249  weniso  7329  abnex  7733  uniuni  7738  frpoins3xp3g  8120  xpord3inddlem  8133  eroveu  8785  fsetexb  8837  mapsnend  9007  isfinite2  9245  marypha1lem  9384  marypha2lem4  9389  infcllem  9439  en3lplem2  9566  cantnfp1  9634  carden2  9940  fseqenlem1  9977  iscard3  10046  cardnum  10047  alephinit  10048  cardinfima  10050  alephiso  10051  dfac10b  10093  dfackm  10120  isfin5-2  10344  brdom7disj  10484  brdom6disj  10485  fsuppmapnn0fiubex  13957  hash2prb  14437  hashle2prv  14443  hashtpg  14450  hash3tpb  14460  swrdnnn0nd  14621  wrd2ind  14688  cshwsexaOLD  14790  s4f1o  14884  cotr2g  14942  relexpindlem  15029  lcmfunsnlem2  16610  ncoprmlnprm  16698  vdwapun  16945  cshwsiun  17070  cshwshash  17075  grpss  18886  symgsubmefmnd  19328  pmtrfrn  19388  pmtrrn2  19390  pmtrprfvalrn  19418  issrg  20097  0ringnnzr  20434  acsfn1p  20708  unocv  21589  dsmmacl  21650  pmatcollpw2lem  22664  fvmptnn04if  22736  toptopon  22804  ordtbas2  23078  ordtrest2  23091  xmeterval  24320  isclmp  24997  ovolfcl  25367  eldv  25799  eltayl  26267  musumsum  27102  2sqreu  27367  2sqreunn  27368  2sqreult  27369  2sqreultb  27370  2sqreunnlt  27371  2sqreunnltb  27372  nosupinfsep  27644  umgrislfupgrlem  29049  numedglnl  29071  ausgrusgrb  29092  cplgr3v  29362  vtxd0nedgb  29416  finsumvtxdg2ssteplem1  29473  isrgr  29487  rgrusgrprc  29517  rgrprcx  29520  upgr2wlk  29596  dfpth2  29659  wwlksnwwlksnon  29845  usgr2wspthon  29895  isclwwlk  29913  clwwlkvbij  30042  iseupthf1o  30131  frcond2  30196  nfrgr2v  30201  4cycl2vnunb  30219  fusgr2wsp2nb  30263  frgrregord013  30324  lejdii  31467  mdslle1i  32246  mdslle2i  32247  mdslj1i  32248  mdslj2i  32249  mo5f  32418  n0nsnel  32444  unipreima  32567  2ndpreima  32631  mgccnv  32925  quslsm  33376  ordtrest2NEW  33913  ordtconnlem1  33914  ballotlem2  34480  plymulx0  34538  bnj115  34715  bnj156  34718  bnj206  34721  bnj110  34848  bnj121  34860  bnj124  34861  bnj130  34864  bnj153  34870  bnj207  34871  bnj581  34898  bnj611  34908  bnj864  34912  bnj865  34913  bnj893  34918  bnj1000  34931  bnj978  34939  bnj1040  34962  bnj1049  34964  bnj1133  34979  bnj1189  34999  satfv1  35350  satfvsucsuc  35352  satfdm  35356  satf0  35359  satf0op  35364  fmlafvel  35372  cnvco1  35746  cnvco2  35747  dfiota3  35911  ss-ax8  36213  trer  36304  nabi1i  36382  nabi2i  36383  bj-hbext  36698  bj-nnfbit  36740  bj-dvelimdv  36839  bj-gabima  36928  bj-elsngl  36956  bj-nuliotaALT  37046  bj-rest10  37076  bj-restuni  37085  con1bii2  37320  con2bii2  37321  topdifinfeq  37338  isbasisrelowllem2  37344  wl-1xor  37470  wl-1mintru1  37476  wl-sb8eut  37566  wl-sb8eutv  37567  inixp  37722  notbinot1  38073  notbinot2  38077  truconj  38095  sbccom2lem  38118  sbccom2  38119  sbccom2f  38120  tsim1  38124  tsxo3  38133  tsxo4  38134  trcoss2  38475  dfcomember3  38666  eqvreldmqs  38667  eqvreldmqs2  38668  dfmembpart2  38762  eldisjn0el  38798  isopos  39173  islvol5  39573  elpadd0  39803  dvhopellsm  41111  diblsmopel  41165  mapdvalc  41623  3factsumint2  42010  3factsumint3  42011  3factsumint4  42012  aks4d1p1p2  42058  aks4d1p7  42071  isprimroot  42081  aks6d1c1p1  42095  aks6d1c2p2  42107  sticksstones22  42156  unitscyglem4  42186  elpwbi  42218  redvmptabs  42348  dffltz  42622  rmxypairf1o  42900  onsupmaxb  43228  ifpnotnotb  43468  ifpdfxor  43476  ifpidg  43480  ifpim123g  43489  ifpim1g  43490  ifpimimb  43493  ifpimim  43498  rp-fakeanorass  43502  elmapintrab  43565  undmrnresiss  43593  clcnvlem  43612  sqrtcvallem1  43620  cnviun  43639  dfxor4  43755  dfhe3  43764  dffrege69  43921  dffrege76  43928  or3or  44012  uneqsn  44014  scottabf  44229  mnurndlem1  44270  ismnushort  44290  pm10.252  44350  pm10.253  44351  pm10.42  44353  aaanv  44377  pm13.195  44402  pm13.196a  44403  sbc3or  44522  en3lpVD  44834  3orbi123VD  44839  sbc3orgVD  44840  sbcoreleleqVD  44848  undif3VD  44871  ax6e2ndeqVD  44898  ax6e2ndeqALT  44920  sineq0ALT  44926  n0abso  44966  permaxsep  44997  permaxinf2lem  45002  uzwo4  45047  iindif2f  45154  allbutfiinf  45416  limsupequzmptlem  45726  cncfshift  45872  dvnmul  45941  dvnprodlem2  45945  rrxsnicc  46298  salexct  46332  sge00  46374  sge0iunmpt  46416  meadjiun  46464  carageneld  46500  ovncvrrp  46562  ovolval4lem1  46647  vonioo  46680  vonicc  46683  nsssmfmbf  46777  smfmullem4  46792  aibandbiaiffaiffb  46895  plcofph  46945  pldofph  46946  plvcofph  46947  plvcofphax  46948  plvofpos  46949  n0nsn2el  47026  fsetsniunop  47050  2reu8i  47114  aovov0bi  47197  tz6.12-afv2  47241  4an21  47271  ichbi12i  47461  ichnfimlem  47464  spr0nelg  47477  sprvalpwn0  47484  reuprpr  47524  requad2  47624  clnbgrel  47829  usgrexmpl2nb4  48026  pg4cyclnex  48117  copisnmnd  48157  pgrpgt2nabl  48354  lindslinindsimp2lem5  48451  islininds2  48473  ldepslinc  48498  line2ylem  48740