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  1501  nornot  1532  truan  1552  truimfal  1565  nottru  1568  falbitru  1571  nic-dfim  1670  nic-dfneg  1671  2nalexn  1829  2nexaln  1831  equvinv  2030  cleljust  2120  sbelx  2256  sb6rfv  2357  cleljustALT  2364  cleljustALT2  2365  dvelimf  2448  sb5rf  2467  sb6rf  2468  sb10f  2527  nexmo  2536  exists2  2657  cleljustab  2712  eqabdv  2864  eqabcri  2875  nne  2932  necon3bbii  2975  necon2abii  2978  necon2bbii  2979  nnel  3042  r19.41v  3162  r3ex  3171  r19.41  3236  rspc2gv  3582  ceqsrexbv  3606  2reu5lem1  3709  2reu5lem2  3710  2reu5lem3  3711  dfsbcq2  3739  cbvreucsf  3889  nss  3994  dfdif3OLD  4067  symdifass  4211  indifdi  4243  difab  4259  neq0  4301  un0  4343  in0  4344  ss0b  4350  2nreu  4393  ralidm  4461  ralf0  4463  reuprg  4655  snssb  4734  snssg  4735  ssunsn2  4778  iindif2  5027  eqsnuniex  5301  nssss  5398  snopeqop  5449  dffr6  5575  epse  5601  rnep  5872  mptpreima  6191  ralrnmpt  7035  fmptsng  7108  fmptsnd  7109  dff14a  7210  f13dfv  7214  weniso  7294  abnex  7696  uniuni  7701  frpoins3xp3g  8077  xpord3inddlem  8090  eroveu  8742  fsetexb  8794  mapsnend  8964  isfinite2  9188  marypha1lem  9323  marypha2lem4  9328  infcllem  9378  en3lplem2  9509  cantnfp1  9577  carden2  9886  fseqenlem1  9921  iscard3  9990  cardnum  9991  alephinit  9992  cardinfima  9994  alephiso  9995  dfac10b  10037  dfackm  10064  isfin5-2  10288  brdom7disj  10428  brdom6disj  10429  fsuppmapnn0fiubex  13905  hash2prb  14385  hashle2prv  14391  hashtpg  14398  hash3tpb  14408  swrdnnn0nd  14570  wrd2ind  14636  s4f1o  14831  cotr2g  14889  relexpindlem  14976  lcmfunsnlem2  16557  ncoprmlnprm  16645  vdwapun  16892  cshwsiun  17017  cshwshash  17022  grpss  18873  symgsubmefmnd  19316  pmtrfrn  19376  pmtrrn2  19378  pmtrprfvalrn  19406  issrg  20112  0ringnnzr  20446  acsfn1p  20720  unocv  21623  dsmmacl  21684  pmatcollpw2lem  22698  fvmptnn04if  22770  toptopon  22838  ordtbas2  23112  ordtrest2  23125  xmeterval  24353  isclmp  25030  ovolfcl  25400  eldv  25832  eltayl  26300  musumsum  27135  2sqreu  27400  2sqreunn  27401  2sqreult  27402  2sqreultb  27403  2sqreunnlt  27404  2sqreunnltb  27405  nosupinfsep  27677  umgrislfupgrlem  29107  numedglnl  29129  ausgrusgrb  29150  cplgr3v  29420  vtxd0nedgb  29474  finsumvtxdg2ssteplem1  29531  isrgr  29545  rgrusgrprc  29575  rgrprcx  29578  upgr2wlk  29652  dfpth2  29714  wwlksnwwlksnon  29900  usgr2wspthon  29953  isclwwlk  29971  clwwlkvbij  30100  iseupthf1o  30189  frcond2  30254  nfrgr2v  30259  4cycl2vnunb  30277  fusgr2wsp2nb  30321  frgrregord013  30382  lejdii  31525  mdslle1i  32304  mdslle2i  32305  mdslj1i  32306  mdslj2i  32307  mo5f  32475  n0nsnel  32502  unipreima  32632  2ndpreima  32696  mgccnv  32987  quslsm  33377  ordtrest2NEW  33943  ordtconnlem1  33944  ballotlem2  34509  plymulx0  34567  bnj115  34744  bnj156  34747  bnj206  34750  bnj110  34877  bnj121  34889  bnj124  34890  bnj130  34893  bnj153  34899  bnj207  34900  bnj581  34927  bnj611  34937  bnj864  34941  bnj865  34942  bnj893  34947  bnj1000  34960  bnj978  34968  bnj1040  34991  bnj1049  34993  bnj1133  35008  bnj1189  35028  satfv1  35414  satfvsucsuc  35416  satfdm  35420  satf0  35423  satf0op  35428  fmlafvel  35436  cnvco1  35810  cnvco2  35811  dfiota3  35972  ss-ax8  36276  trer  36367  nabi1i  36445  nabi2i  36446  bj-hbext  36761  bj-nnfbit  36803  bj-dvelimdv  36902  bj-gabima  36991  bj-elsngl  37019  bj-nuliotaALT  37109  bj-rest10  37139  bj-restuni  37148  con1bii2  37383  con2bii2  37384  topdifinfeq  37401  isbasisrelowllem2  37407  wl-1xor  37533  wl-1mintru1  37539  wl-sb8eut  37629  wl-sb8eutv  37630  inixp  37774  notbinot1  38125  notbinot2  38129  truconj  38147  sbccom2lem  38170  sbccom2  38171  sbccom2f  38172  tsim1  38176  tsxo3  38185  tsxo4  38186  trcoss2  38592  dfcomember3  38778  eqvreldmqs  38779  eqvreldmqs2  38780  dfmembpart2  38874  eldisjn0el  38910  isopos  39285  islvol5  39684  elpadd0  39914  dvhopellsm  41222  diblsmopel  41276  mapdvalc  41734  3factsumint2  42121  3factsumint3  42122  3factsumint4  42123  aks4d1p1p2  42169  aks4d1p7  42182  isprimroot  42192  aks6d1c1p1  42206  aks6d1c2p2  42218  sticksstones22  42267  unitscyglem4  42297  elpwbi  42329  redvmptabs  42459  dffltz  42733  rmxypairf1o  43009  onsupmaxb  43337  ifpnotnotb  43577  ifpdfxor  43585  ifpidg  43589  ifpim123g  43598  ifpim1g  43599  ifpimimb  43602  ifpimim  43607  rp-fakeanorass  43611  elmapintrab  43674  undmrnresiss  43702  clcnvlem  43721  sqrtcvallem1  43729  cnviun  43748  dfxor4  43864  dfhe3  43873  dffrege69  44030  dffrege76  44037  or3or  44121  uneqsn  44123  scottabf  44338  mnurndlem1  44379  ismnushort  44399  pm10.252  44459  pm10.253  44460  pm10.42  44462  aaanv  44486  pm13.195  44511  pm13.196a  44512  sbc3or  44630  en3lpVD  44942  3orbi123VD  44947  sbc3orgVD  44948  sbcoreleleqVD  44956  undif3VD  44979  ax6e2ndeqVD  45006  ax6e2ndeqALT  45028  sineq0ALT  45034  n0abso  45074  permaxsep  45105  permaxinf2lem  45110  uzwo4  45155  iindif2f  45262  allbutfiinf  45523  limsupequzmptlem  45831  cncfshift  45977  dvnmul  46046  dvnprodlem2  46050  rrxsnicc  46403  salexct  46437  sge00  46479  sge0iunmpt  46521  meadjiun  46569  carageneld  46605  ovncvrrp  46667  ovolval4lem1  46752  vonioo  46785  vonicc  46788  nsssmfmbf  46882  smfmullem4  46897  aibandbiaiffaiffb  46999  plcofph  47049  pldofph  47050  plvcofph  47051  plvcofphax  47052  plvofpos  47053  n0nsn2el  47130  fsetsniunop  47154  2reu8i  47218  aovov0bi  47301  tz6.12-afv2  47345  4an21  47375  ichbi12i  47565  ichnfimlem  47568  spr0nelg  47581  sprvalpwn0  47588  reuprpr  47628  requad2  47728  clnbgrel  47933  usgrexmpl2nb4  48140  pg4cyclnex  48232  copisnmnd  48274  pgrpgt2nabl  48471  lindslinindsimp2lem5  48568  islininds2  48590  ldepslinc  48615  line2ylem  48857