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  2028  cleljust  2117  sbelx  2253  sb6rfv  2359  cleljustALT  2366  cleljustALT2  2367  dvelimf  2452  sb5rf  2471  sb6rf  2472  sb10f  2531  nexmo  2540  exists2  2661  cleljustab  2716  eqabdv  2868  eqabcri  2879  nne  2936  necon3bbii  2979  necon2abii  2982  necon2bbii  2983  nnel  3046  r19.41v  3174  r3ex  3183  r19.41  3246  rspc2gv  3611  ceqsrexbv  3635  rabeqcOLD  3669  2reu5lem1  3738  2reu5lem2  3739  2reu5lem3  3740  dfsbcq2  3768  cbvreucsf  3918  nss  4023  dfdif3OLD  4093  symdifass  4237  indifdi  4269  difab  4285  neq0  4327  un0  4369  in0  4370  ss0b  4376  eq0rdv  4382  2nreu  4419  ralidm  4487  ralf0  4489  reuprg  4679  snssb  4758  snssg  4759  ssunsn2  4803  iindif2  5053  eqsnuniex  5331  nssss  5430  snopeqop  5481  dffr6  5609  epse  5636  rnep  5906  cotrgOLDOLD  6098  mptpreima  6227  ralrnmpt  7085  fmptsng  7159  fmptsnd  7160  dff14a  7262  f13dfv  7266  weniso  7346  abnex  7749  uniuni  7754  frpoins3xp3g  8138  xpord3inddlem  8151  eroveu  8824  fsetexb  8876  mapsnend  9048  isfinite2  9304  marypha1lem  9443  marypha2lem4  9448  infcllem  9498  en3lplem2  9625  cantnfp1  9693  carden2  9999  fseqenlem1  10036  iscard3  10105  cardnum  10106  alephinit  10107  cardinfima  10109  alephiso  10110  dfac10b  10152  dfackm  10179  isfin5-2  10403  brdom7disj  10543  brdom6disj  10544  fsuppmapnn0fiubex  14008  hash2prb  14488  hashle2prv  14494  hashtpg  14501  hash3tpb  14511  swrdnnn0nd  14672  wrd2ind  14739  cshwsexaOLD  14841  s4f1o  14935  cotr2g  14993  relexpindlem  15080  lcmfunsnlem2  16657  ncoprmlnprm  16745  vdwapun  16992  cshwsiun  17117  cshwshash  17122  grpss  18935  symgsubmefmnd  19377  pmtrfrn  19437  pmtrrn2  19439  pmtrprfvalrn  19467  issrg  20146  0ringnnzr  20483  acsfn1p  20757  unocv  21638  dsmmacl  21699  pmatcollpw2lem  22713  fvmptnn04if  22785  toptopon  22853  ordtbas2  23127  ordtrest2  23140  xmeterval  24369  isclmp  25046  ovolfcl  25417  eldv  25849  eltayl  26317  musumsum  27152  2sqreu  27417  2sqreunn  27418  2sqreult  27419  2sqreultb  27420  2sqreunnlt  27421  2sqreunnltb  27422  nosupinfsep  27694  umgrislfupgrlem  29047  numedglnl  29069  ausgrusgrb  29090  cplgr3v  29360  vtxd0nedgb  29414  finsumvtxdg2ssteplem1  29471  isrgr  29485  rgrusgrprc  29515  rgrprcx  29518  upgr2wlk  29594  dfpth2  29657  wwlksnwwlksnon  29843  usgr2wspthon  29893  isclwwlk  29911  clwwlkvbij  30040  iseupthf1o  30129  frcond2  30194  nfrgr2v  30199  4cycl2vnunb  30217  fusgr2wsp2nb  30261  frgrregord013  30322  lejdii  31465  mdslle1i  32244  mdslle2i  32245  mdslj1i  32246  mdslj2i  32247  mo5f  32416  n0nsnel  32442  unipreima  32567  2ndpreima  32631  mgccnv  32925  quslsm  33366  ordtrest2NEW  33900  ordtconnlem1  33901  ballotlem2  34467  plymulx0  34525  bnj115  34702  bnj156  34705  bnj206  34708  bnj110  34835  bnj121  34847  bnj124  34848  bnj130  34851  bnj153  34857  bnj207  34858  bnj581  34885  bnj611  34895  bnj864  34899  bnj865  34900  bnj893  34905  bnj1000  34918  bnj978  34926  bnj1040  34949  bnj1049  34951  bnj1133  34966  bnj1189  34986  satfv1  35331  satfvsucsuc  35333  satfdm  35337  satf0  35340  satf0op  35345  fmlafvel  35353  cnvco1  35722  cnvco2  35723  dfiota3  35887  ss-ax8  36189  trer  36280  nabi1i  36358  nabi2i  36359  bj-hbext  36674  bj-nnfbit  36716  bj-dvelimdv  36815  bj-gabima  36904  bj-elsngl  36932  bj-nuliotaALT  37022  bj-rest10  37052  bj-restuni  37061  con1bii2  37296  con2bii2  37297  topdifinfeq  37314  isbasisrelowllem2  37320  wl-1xor  37446  wl-1mintru1  37452  wl-sb8eut  37542  wl-sb8eutv  37543  inixp  37698  notbinot1  38049  notbinot2  38053  truconj  38071  sbccom2lem  38094  sbccom2  38095  sbccom2f  38096  tsim1  38100  tsxo3  38109  tsxo4  38110  trcoss2  38448  dfcomember3  38638  eqvreldmqs  38639  eqvreldmqs2  38640  dfmembpart2  38734  eldisjn0el  38770  isopos  39144  islvol5  39544  elpadd0  39774  dvhopellsm  41082  diblsmopel  41136  mapdvalc  41594  3factsumint2  41981  3factsumint3  41982  3factsumint4  41983  aks4d1p1p2  42029  aks4d1p7  42042  isprimroot  42052  aks6d1c1p1  42066  aks6d1c2p2  42078  sticksstones22  42127  unitscyglem4  42157  elpwbi  42227  redvmptabs  42350  dffltz  42604  rmxypairf1o  42882  onsupmaxb  43210  ifpnotnotb  43450  ifpdfxor  43458  ifpidg  43462  ifpim123g  43471  ifpim1g  43472  ifpimimb  43475  ifpimim  43480  rp-fakeanorass  43484  elmapintrab  43547  undmrnresiss  43575  clcnvlem  43594  sqrtcvallem1  43602  cnviun  43621  dfxor4  43737  dfhe3  43746  dffrege69  43903  dffrege76  43910  or3or  43994  uneqsn  43996  scottabf  44212  mnurndlem1  44253  ismnushort  44273  pm10.252  44333  pm10.253  44334  pm10.42  44336  aaanv  44360  pm13.195  44385  pm13.196a  44386  sbc3or  44505  en3lpVD  44817  3orbi123VD  44822  sbc3orgVD  44823  sbcoreleleqVD  44831  undif3VD  44854  ax6e2ndeqVD  44881  ax6e2ndeqALT  44903  sineq0ALT  44909  n0abso  44949  permaxsep  44980  permaxinf2lem  44985  uzwo4  45025  iindif2f  45132  allbutfiinf  45395  limsupequzmptlem  45705  cncfshift  45851  dvnmul  45920  dvnprodlem2  45924  rrxsnicc  46277  salexct  46311  sge00  46353  sge0iunmpt  46395  meadjiun  46443  carageneld  46479  ovncvrrp  46541  ovolval4lem1  46626  vonioo  46659  vonicc  46662  nsssmfmbf  46756  smfmullem4  46771  aibandbiaiffaiffb  46871  plcofph  46921  pldofph  46922  plvcofph  46923  plvcofphax  46924  plvofpos  46925  n0nsn2el  47002  fsetsniunop  47026  2reu8i  47090  aovov0bi  47173  tz6.12-afv2  47217  4an21  47247  ichbi12i  47422  ichnfimlem  47425  spr0nelg  47438  sprvalpwn0  47445  reuprpr  47485  requad2  47585  clnbgrel  47790  usgrexmpl2nb4  47987  copisnmnd  48092  pgrpgt2nabl  48289  lindslinindsimp2lem5  48386  islininds2  48408  ldepslinc  48433  line2ylem  48679