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  645  an43  659  anabs1  663  anabs7  665  pm4.87  844  pm4.64  850  pm4.25  906  pm4.77  965  pm4.53  988  pm4.55  990  pm4.56  991  pm4.57  993  pm5.63  1022  3anor  1108  3oran  1109  syl3anbr  1163  3an6  1449  nanbi  1502  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1671  nic-dfneg  1672  2nalexn  1830  2nexaln  1832  equvinv  2031  cleljust  2123  sbelx  2260  sb6rfv  2360  cleljustALT  2367  cleljustALT2  2368  dvelimf  2451  sb5rf  2470  sb6rf  2471  sb10f  2530  nexmo  2540  exists2  2661  cleljustab  2716  eqabdv  2868  eqabcri  2878  nne  2934  necon3bbii  2977  necon2abii  2980  necon2bbii  2981  nnel  3044  r19.41v  3165  r3ex  3174  r19.41  3239  rspc2gv  3572  ceqsrexbv  3596  2reu5lem1  3698  2reu5lem2  3699  2reu5lem3  3700  dfsbcq2  3728  cbvreucsf  3877  nss  3981  dfdif3OLD  4051  symdifass  4192  indifdi  4224  difab  4240  neq0  4282  un0  4324  in0  4325  ss0b  4331  2nreu  4374  ralidm  4447  reuprg  4637  snssb  4716  snssg  4717  ssunsn2  4760  iindif2  5008  eqsnuniex  5292  nssss  5396  snopeqop  5449  dffr6  5576  epse  5602  rnep  5871  mptpreima  6191  ralrnmpt  7037  fmptsng  7112  fmptsnd  7113  dff14a  7214  f13dfv  7218  weniso  7298  abnex  7700  uniuni  7705  frpoins3xp3g  8080  xpord3inddlem  8093  eroveu  8748  fsetexb  8800  mapsnend  8972  isfinite2  9197  marypha1lem  9335  marypha2lem4  9340  infcllem  9390  en3lplem2  9523  cantnfp1  9591  carden2  9900  fseqenlem1  9935  iscard3  10004  cardnum  10005  alephinit  10006  cardinfima  10008  alephiso  10009  dfac10b  10051  dfackm  10078  isfin5-2  10302  brdom7disj  10442  brdom6disj  10443  fsuppmapnn0fiubex  13943  hash2prb  14423  hashle2prv  14429  hashtpg  14436  hash3tpb  14446  swrdnnn0nd  14608  wrd2ind  14674  s4f1o  14869  cotr2g  14927  relexpindlem  15014  lcmfunsnlem2  16598  ncoprmlnprm  16687  vdwapun  16934  cshwsiun  17059  cshwshash  17064  grpss  18919  symgsubmefmnd  19362  pmtrfrn  19422  pmtrrn2  19424  pmtrprfvalrn  19452  issrg  20158  0ringnnzr  20491  acsfn1p  20765  unocv  21649  dsmmacl  21710  pmatcollpw2lem  22730  fvmptnn04if  22802  toptopon  22870  ordtbas2  23144  ordtrest2  23157  xmeterval  24385  isclmp  25052  ovolfcl  25421  eldv  25853  eltayl  26313  musumsum  27143  2sqreu  27407  2sqreunn  27408  2sqreult  27409  2sqreultb  27410  2sqreunnlt  27411  2sqreunnltb  27412  nosupinfsep  27684  umgrislfupgrlem  29179  numedglnl  29201  ausgrusgrb  29222  cplgr3v  29492  vtxd0nedgb  29545  finsumvtxdg2ssteplem1  29602  isrgr  29616  rgrusgrprc  29646  rgrprcx  29649  upgr2wlk  29723  dfpth2  29785  wwlksnwwlksnon  29971  usgr2wspthon  30024  isclwwlk  30042  clwwlkvbij  30171  iseupthf1o  30260  frcond2  30325  nfrgr2v  30330  4cycl2vnunb  30348  fusgr2wsp2nb  30392  frgrregord013  30453  lejdii  31597  mdslle1i  32376  mdslle2i  32377  mdslj1i  32378  mdslj2i  32379  mo5f  32546  n0nsnel  32573  unipreima  32704  2ndpreima  32769  mgccnv  33047  domnprodeq0  33325  quslsm  33453  mplmonprod  33686  ordtrest2NEW  34055  ordtconnlem1  34056  ballotlem2  34621  plymulx0  34679  bnj115  34856  bnj156  34859  bnj206  34862  bnj110  34988  bnj121  35000  bnj124  35001  bnj130  35004  bnj153  35010  bnj207  35011  bnj581  35038  bnj611  35048  bnj864  35052  bnj865  35053  bnj893  35058  bnj1000  35071  bnj978  35079  bnj1040  35102  bnj1049  35104  bnj1133  35119  bnj1189  35139  satfv1  35533  satfvsucsuc  35535  satfdm  35539  satf0  35542  satf0op  35547  fmlafvel  35555  cnvco1  35929  cnvco2  35930  dfiota3  36091  ss-ax8  36395  trer  36486  nabi1i  36564  nabi2i  36565  regsfromregtco  36708  bj-nnfbit  37043  bj-dvelimdv  37146  bj-gabima  37235  bj-elsngl  37263  bj-nuliotaALT  37353  bj-axseprep  37369  bj-rest10  37388  bj-restuni  37397  con1bii2  37636  con2bii2  37637  topdifinfeq  37654  isbasisrelowllem2  37660  wl-1xor  37786  wl-1mintru1  37792  wl-sb8eut  37891  wl-sb8eutv  37892  inixp  38037  notbinot1  38388  notbinot2  38392  truconj  38410  sbccom2lem  38433  sbccom2  38434  sbccom2f  38435  tsim1  38439  tsxo3  38448  tsxo4  38449  trcoss2  38883  dfcomember3  39068  eqvreldmqs  39069  eqvreldmqs2  39070  dfmembpart2  39182  eldisjn0el  39218  isopos  39614  islvol5  40013  elpadd0  40243  dvhopellsm  41551  diblsmopel  41605  mapdvalc  42063  3factsumint2  42449  3factsumint3  42450  3factsumint4  42451  aks4d1p1p2  42497  aks4d1p7  42510  isprimroot  42520  aks6d1c1p1  42534  aks6d1c2p2  42546  sticksstones22  42595  unitscyglem4  42625  elpwbi  42659  redvmptabs  42780  dffltz  43055  rmxypairf1o  43327  onsupmaxb  43655  ifpnotnotb  43894  ifpdfxor  43902  ifpidg  43906  ifpim123g  43915  ifpim1g  43916  ifpimimb  43919  ifpimim  43924  rp-fakeanorass  43928  elmapintrab  43991  undmrnresiss  44019  clcnvlem  44038  sqrtcvallem1  44046  cnviun  44065  dfxor4  44181  dfhe3  44190  dffrege69  44347  dffrege76  44354  or3or  44438  uneqsn  44440  scottabf  44655  mnurndlem1  44696  ismnushort  44716  pm10.252  44776  pm10.253  44777  pm10.42  44779  aaanv  44803  pm13.195  44828  pm13.196a  44829  sbc3or  44947  en3lpVD  45259  3orbi123VD  45264  sbc3orgVD  45265  sbcoreleleqVD  45273  undif3VD  45296  ax6e2ndeqVD  45323  ax6e2ndeqALT  45345  sineq0ALT  45351  n0abso  45391  permaxsep  45422  permaxinf2lem  45427  uzwo4  45472  iindif2f  45578  allbutfiinf  45836  limsupequzmptlem  46144  cncfshift  46290  dvnmul  46359  dvnprodlem2  46363  rrxsnicc  46716  salexct  46750  sge00  46792  sge0iunmpt  46834  meadjiun  46882  carageneld  46918  ovncvrrp  46980  ovolval4lem1  47065  vonioo  47098  vonicc  47101  nsssmfmbf  47195  smfmullem4  47210  aibandbiaiffaiffb  47330  plcofph  47380  pldofph  47381  plvcofph  47382  plvcofphax  47383  plvofpos  47384  n0nsn2el  47461  fsetsniunop  47485  2reu8i  47549  aovov0bi  47632  tz6.12-afv2  47676  4an21  47706  ichbi12i  47908  ichnfimlem  47911  spr0nelg  47924  sprvalpwn0  47931  reuprpr  47971  nprmmul1  47975  requad2  48087  clnbgrel  48292  usgrexmpl2nb4  48499  pg4cyclnex  48591  copisnmnd  48633  pgrpgt2nabl  48830  lindslinindsimp2lem5  48926  islininds2  48948  ldepslinc  48973  line2ylem  49215