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  1475  nanbi  1529  nornot  1560  truan  1580  truimfal  1593  nottru  1596  falbitru  1599  had0  1633  nic-dfim  1701  nic-dfneg  1702  2nalexn  1860  2nexaln  1862  equvinv  2061  cleljust  2153  sbelx  2288  sb6rfv  2386  cleljustALT  2393  cleljustALT2  2394  dvelimf  2477  sb5rf  2496  sb6rf  2497  sb10f  2556  nexmo  2566  exists2  2686  cleljustab  2741  eqabdv  2893  eqabcri  2903  nne  2959  necon3bbii  3002  necon2abii  3005  necon2bbii  3006  nnel  3071  r19.41v  3192  r3ex  3201  r19.41  3266  rspc2gv  3585  ceqsrexbv  3609  2reu5lem1  3712  2reu5lem2  3713  2reu5lem3  3714  dfsbcq2  3741  cbvreucsf  3890  nss  3972  symdifass  4207  indifdi  4239  difab  4255  neq0  4298  un0  4343  in0  4344  ss0b  4350  2nreu  4401  ralidm  4472  reuprg  4663  snssb  4742  snssg  4743  ssunsn2  4787  iindif2  5036  eqsnuniex  5322  nssss  5422  snopeqop  5477  dffr6  5606  epse  5632  rnep  5908  mptpreima  6239  ralrnmpt  7096  fmptsng  7173  fmptsnd  7174  dff14a  7274  f13dfv  7282  weniso  7364  abnex  7771  uniuni  7776  frpoins3xp3g  8158  xpord3inddlem  8171  eroveu  8833  fsetexb  8886  mapsnend  9064  isfinite2  9290  marypha1lem  9425  marypha2lem4  9430  infcllem  9480  en3lplem2  9614  cantnfp1  9682  scottabf  9939  carden2  10068  fseqenlem1  10103  iscard3  10172  cardnum  10173  alephinit  10174  cardinfima  10176  alephiso  10177  dfac10b  10218  dfackm  10245  isfin5-2  10469  brdom7disj  10610  brdom6disj  10611  fsuppmapnn0fiubex  14135  hash2prb  14617  hashle2prv  14623  hashtpg  14630  hash3tpb  14640  swrdnnn0nd  14806  wrd2ind  14872  s4f1o  15069  cotr2g  15129  relexpindlem  15216  lcmfunsnlem2  16815  ncoprmlnprm  16904  vdwapun  17152  cshwsiun  17277  cshwshash  17282  degenmgm2nfun  19139  grpss  19165  symgsubmefmnd  19612  pmtrfrn  19672  pmtrrn2  19674  pmtrprfvalrn  19702  issrg  20414  dfring3  20518  0ringnnzr  20776  acsfn1p  21056  unocv  21986  dsmmacl  22047  pmatcollpw2lem  23095  fvmptnn04if  23167  toptopon  23235  ordtbas2  23509  ordtrest2  23522  xmeterval  24751  isclmp  25418  ovolfcl  25787  eldv  26218  plyn0mulidp  26602  eltayl  26687  musumsum  27519  2sqreu  27783  2sqreunn  27784  2sqreult  27785  2sqreultb  27786  2sqreunnlt  27787  2sqreunnltb  27788  nosupinfsep  28089  umgrislfupgrlem  29700  numedglnl  29722  ausgrusgrb  29746  cplgr3v  30016  vtxd0nedgb  30069  finsumvtxdg2ssteplem1  30126  isrgr  30140  rgrusgrprc  30170  rgrprcx  30173  upgr2wlk  30247  dfpth2  30314  wwlksnwwlksnon  30504  usgr2wspthon  30557  isclwwlk  30575  clwwlkvbij  30704  iseupthf1o  30803  frcond2  30868  nfrgr2v  30873  4cycl2vnunb  30891  fusgr2wsp2nb  30935  frgrregord013  30996  lejdii  32140  mdslle1i  32919  mdslle2i  32920  mdslj1i  32921  mdslj2i  32922  mo5f  33085  n0nsnel  33111  unipreima  33237  2ndpreima  33301  mgccnv  33560  domnprodeq0  33840  quslsm  33956  mplmonprod  34186  ordtrest2NEW  34555  ordtconnlem1  34556  ballotlem2  35121  bnj115  35356  bnj156  35359  bnj206  35362  bnj110  35488  bnj121  35500  bnj124  35501  bnj130  35504  bnj153  35510  bnj207  35511  bnj581  35538  bnj611  35548  bnj864  35552  bnj865  35553  bnj893  35558  bnj1000  35571  bnj978  35579  bnj1040  35602  bnj1049  35604  bnj1133  35619  bnj1189  35639  satfv1  36128  satfvsucsuc  36130  satfdm  36134  satf0  36137  satf0op  36142  fmlafvel  36150  cnvco1  36524  cnvco2  36525  dfiota3  36685  ss-ax8  37014  trer  37104  nabi1i  37182  nabi2i  37183  regsfromregtco  37326  bj-nnfbit  37660  bj-dvelimdv  37763  bj-gabima  37853  bj-elsngl  37881  bj-nuliotaALT  37973  bj-axseprep  37990  bj-rest10  38009  bj-restuni  38018  con1bii2  38256  con2bii2  38257  topdifinfeq  38274  isbasisrelowllem2  38280  wl-1xor  38406  wl-1mintru1  38412  wl-sb8eut  38511  wl-sb8eutv  38512  inixp  38663  notbinot1  39014  notbinot2  39018  truconj  39034  sbccom2lem  39057  sbccom2  39058  sbccom2f  39059  tsim1  39063  tsxo3  39072  tsxo4  39073  trcoss2  39507  dfcomember3  39692  eqvreldmqs  39693  eqvreldmqs2  39694  dfmembpart2  39806  eldisjn0el  39842  isopos  40238  islvol5  40637  elpadd0  40867  dvhopellsm  42175  diblsmopel  42229  mapdvalc  42687  3factsumint2  43073  3factsumint3  43074  3factsumint4  43075  aks4d1p1p2  43121  aks4d1p7  43134  isprimroot  43144  aks6d1c1p1  43158  aks6d1c2p2  43170  sticksstones22  43219  unitscyglem4  43249  elpwbi  43285  redvmptabs  43412  dffltz  43671  rmxypairf1o  43918  onsupmaxb  44241  ifpnotnotb  44480  ifpdfxor  44488  ifpidg  44492  ifpim123g  44501  ifpim1g  44502  ifpimimb  44505  ifpimim  44510  rp-fakeanorass  44514  elmapintrab  44577  undmrnresiss  44604  clcnvlem  44623  sqrtcvallem1  44631  cnviun  44650  dfxor4  44766  dfhe3  44775  dffrege69  44932  dffrege76  44939  or3or  45023  uneqsn  45025  mnurndlem1  45265  ismnushort  45285  pm10.252  45345  pm10.253  45346  pm10.42  45348  aaanv  45372  pm13.195  45397  pm13.196a  45398  sbc3or  45515  en3lpVD  45827  3orbi123VD  45832  sbc3orgVD  45833  sbcoreleleqVD  45841  undif3VD  45864  ax6e2ndeqVD  45891  ax6e2ndeqALT  45913  sineq0ALT  45919  n0abso  45966  permaxsep  45997  permaxinf2lem  46002  iindif2f  46175  allbutfiinf  46430  limsupequzmptlem  46738  cncfshift  46884  dvnmul  46953  dvnprodlem2  46957  rrxsnicc  47310  sge00  47386  sge0iunmpt  47428  meadjiun  47476  ovolval4lem1  47659  nsssmfmbf  47789  smfmullem4  47804  aibandbiaiffaiffb  47964  plcofph  48014  pldofph  48015  plvcofph  48016  plvcofphax  48017  plvofpos  48018  n0nsn2el  48095  fsetsniunop  48119  2reu8i  48183  aovov0bi  48266  tz6.12-afv2  48310  4an21  48340  ichbi12i  48542  ichnfimlem  48545  spr0nelg  48558  sprvalpwn0  48565  reuprpr  48605  nprmmul1  48609  requad2  48721  clnbgrel  48926  usgrexmpl2nb4  49133  pg4cyclnex  49225  copisnmnd  49266  isprmrng  49433  pgrpgt2nabl  49478  lindslinindsimp2lem5  49574  islininds2  49596  ldepslinc  49621  line2ylem  49863  alsanmo  50906  ralsanmo  50907  alsralrex  50908  2alsraln0id  50914