Theorem bicomi 227

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 224	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpri  231  bitr2i  279  bitr3i  280  bitr4i  281  bitr3id  288  bitr3di  289  bitr4di  292  bitr4id  293  mtbir  326  sylnibr  332  sylnbir  334  xchnxbir  336  xchbinxr  338  con1bii  359  nbn  375  xor3  385  pm5.41  395  pm4.63  403  pm4.61  410  pm4.76  528  anidm  575  an21  657  an43  671  anabs1  675  anabs7  677  pm4.87  857  pm4.64  863  pm4.25  919  pm4.77  977  pm4.53  1001  pm4.55  1003  pm4.56  1004  pm4.57  1006  pm5.63  1037  3anor  1125  3oran  1126  syl3anbr  1180  3an6  1476  nanbi  1530  nornot  1561  truan  1581  truimfal  1594  nottru  1597  falbitru  1600  had0  1634  nic-dfim  1702  nic-dfneg  1703  2nalexn  1861  2nexaln  1863  equvinv  2064  cleljust  2156  sbelx  2292  sb6rfv  2389  cleljustALT  2396  cleljustALT2  2397  dvelimf  2480  sb5rf  2499  sb6rf  2500  sb10f  2559  nexmo  2569  exists2  2689  cleljustab  2744  eqabdv  2897  eqabcri  2907  nne  2963  necon3bbii  3006  necon2abii  3009  necon2bbii  3010  nnel  3075  r19.41v  3196  r3ex  3205  r19.41  3270  rspc2gv  3589  ceqsrexbv  3613  2reu5lem1  3716  2reu5lem2  3717  2reu5lem3  3718  dfsbcq2  3745  cbvreucsf  3895  nss  3977  symdifass  4210  indifdi  4242  difab  4258  neq0  4302  un0  4347  in0  4348  ss0b  4354  2nreu  4405  ralidm  4476  reuprg  4664  snssb  4743  snssg  4744  ssunsn2  4786  iindif2  5040  eqsnuniex  5327  nssss  5427  snopeqop  5482  dffr6  5611  epse  5637  rnep  5915  mptpreima  6251  ralrnmpt  7117  fmptsng  7193  fmptsnd  7194  dff14a  7294  f13dfv  7302  weniso  7384  abnex  7792  uniuni  7797  frpoins3xp3g  8182  xpord3inddlem  8195  eroveu  8858  fsetexb  8911  mapsnend  9089  isfinite2  9315  marypha1lem  9449  marypha2lem4  9454  infcllem  9504  en3lplem2  9638  cantnfp1  9706  scottabf  9963  carden2  10092  fseqenlem1  10127  iscard3  10196  cardnum  10197  alephinit  10198  cardinfima  10200  alephiso  10201  dfac10b  10242  dfackm  10269  isfin5-2  10493  brdom7disj  10634  brdom6disj  10635  fsuppmapnn0fiubex  14159  hash2prb  14641  hashle2prv  14647  hashtpg  14654  hash3tpb  14664  swrdnnn0nd  14831  wrd2ind  14897  s4f1o  15095  cotr2g  15155  relexpindlem  15242  lcmfunsnlem2  16841  ncoprmlnprm  16930  vdwapun  17178  cshwsiun  17303  cshwshash  17308  degenmgm2nfun  19165  grpss  19191  symgsubmefmnd  19639  pmtrfrn  19699  pmtrrn2  19701  pmtrprfvalrn  19729  issrg  20441  dfring3  20545  0ringnnzr  20803  acsfn1p  21083  unocv  22013  dsmmacl  22074  pmatcollpw2lem  23122  fvmptnn04if  23194  toptopon  23262  ordtbas2  23536  ordtrest2  23549  xmeterval  24778  isclmp  25445  ovolfcl  25814  eldv  26245  plyn0mulidp  26629  eltayl  26714  musumsum  27546  2sqreu  27810  2sqreunn  27811  2sqreult  27812  2sqreultb  27813  2sqreunnlt  27814  2sqreunnltb  27815  nosupinfsep  28116  umgrislfupgrlem  29727  numedglnl  29749  ausgrusgrb  29773  cplgr3v  30043  vtxd0nedgb  30096  finsumvtxdg2ssteplem1  30153  isrgr  30167  rgrusgrprc  30197  rgrprcx  30200  upgr2wlk  30274  dfpth2  30341  wwlksnwwlksnon  30531  usgr2wspthon  30584  isclwwlk  30602  clwwlkvbij  30731  iseupthf1o  30830  frcond2  30895  nfrgr2v  30900  4cycl2vnunb  30918  fusgr2wsp2nb  30962  frgrregord013  31023  lejdii  32167  mdslle1i  32946  mdslle2i  32947  mdslj1i  32948  mdslj2i  32949  mo5f  33154  n0nsnel  33180  unipreima  33306  2ndpreima  33369  mgccnv  33627  domnprodeq0  33907  quslsm  34023  mplmonprod  34253  ordtrest2NEW  34622  ordtconnlem1  34623  ballotlem2  35188  bnj115  35423  bnj156  35426  bnj206  35429  bnj110  35555  bnj121  35567  bnj124  35568  bnj130  35571  bnj153  35577  bnj207  35578  bnj581  35605  bnj611  35615  bnj864  35619  bnj865  35620  bnj893  35625  bnj1000  35638  bnj978  35646  bnj1040  35669  bnj1049  35671  bnj1133  35686  bnj1189  35706  satfv1  36294  satfvsucsuc  36296  satfdm  36300  satf0  36303  satf0op  36308  fmlafvel  36316  cnvco1  36701  cnvco2  36702  dfiota3  36862  ss-ax8  37191  trer  37281  nabi1i  37359  nabi2i  37360  regsfromregtco  37503  bj-nnfbit  37837  bj-dvelimdv  37940  bj-gabima  38030  bj-elsngl  38058  relpart  38142  bj-nuliotaALT  38163  bj-axseprep  38180  bj-rest10  38199  bj-restuni  38208  con1bii2  38446  con2bii2  38447  topdifinfeq  38464  isbasisrelowllem2  38470  wl-1xor  38596  wl-1mintru1  38602  wl-sb8eut  38701  wl-sb8eutv  38702  inixp  38853  notbinot1  39204  notbinot2  39208  truconj  39224  sbccom2lem  39247  sbccom2  39248  sbccom2f  39249  tsim1  39253  tsxo3  39262  tsxo4  39263  trcoss2  39697  dfcomember3  39882  eqvreldmqs  39883  eqvreldmqs2  39884  dfmembpart2  39996  eldisjn0el  40032  isopos  40428  islvol5  40827  elpadd0  41057  dvhopellsm  42365  diblsmopel  42419  mapdvalc  42877  3factsumint2  43263  3factsumint3  43264  3factsumint4  43265  aks4d1p1p2  43311  aks4d1p7  43324  isprimroot  43334  aks6d1c1p1  43348  aks6d1c2p2  43360  sticksstones22  43409  unitscyglem4  43439  elpwbi  43475  redvmptabs  43602  dffltz  43861  rmxypairf1o  44109  onsupmaxb  44431  ifpnotnotb  44670  ifpdfxor  44678  ifpidg  44682  ifpim123g  44691  ifpim1g  44692  ifpimimb  44695  ifpimim  44700  rp-fakeanorass  44704  elmapintrab  44767  undmrnresiss  44794  clcnvlem  44813  sqrtcvallem1  44821  cnviun  44840  dfxor4  44956  dfhe3  44965  dffrege69  45122  dffrege76  45129  or3or  45213  uneqsn  45215  mnurndlem1  45455  ismnushort  45475  pm10.252  45535  pm10.253  45536  pm10.42  45538  aaanv  45562  pm13.195  45587  pm13.196a  45588  sbc3or  45704  en3lpVD  46016  3orbi123VD  46021  sbc3orgVD  46022  sbcoreleleqVD  46030  undif3VD  46053  ax6e2ndeqVD  46080  ax6e2ndeqALT  46102  sineq0ALT  46108  n0abso  46159  permaxsep  46190  permaxinf2lem  46195  iindif2f  46378  allbutfiinf  46633  limsupequzmptlem  46941  cncfshift  47087  dvnmul  47156  dvnprodlem2  47160  rrxsnicc  47513  sge00  47589  sge0iunmpt  47631  meadjiun  47679  ovolval4lem1  47862  nsssmfmbf  47992  smfmullem4  48007  aibandbiaiffaiffb  48167  plcofph  48217  pldofph  48218  plvcofph  48219  plvcofphax  48220  plvofpos  48221  n0nsn2el  48298  fsetsniunop  48322  2reu8i  48387  aovov0bi  48469  tz6.12-afv2  48513  4an21  48543  ichbi12i  48745  ichnfimlem  48748  spr0nelg  48761  sprvalpwn0  48768  reuprpr  48808  nprmmul1  48812  requad2  48924  clnbgrel  49129  usgrexmpl2nb4  49336  pg4cyclnex  49428  copisnmnd  49469  isprmrng  49636  pgrpgt2nabl  49681  lindslinindsimp2lem5  49777  islininds2  49799  ldepslinc  49824  line2ylem  50066  alsanmo  51184  ralsanmo  51185  alsralrex  51186  2alsraln0id  51192