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 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced 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  394  pm4.63  402  pm4.61  409  pm4.76  527  anidm  574  an21  656  an43  670  anabs1  674  anabs7  676  pm4.87  856  pm4.64  862  pm4.25  918  pm4.77  977  pm4.53  1001  pm4.55  1003  pm4.56  1004  pm4.57  1006  pm5.63  1035  3anor  1123  3oran  1124  syl3anbr  1178  3an6  1473  nanbi  1528  nornot  1559  truan  1579  truimfal  1592  nottru  1595  falbitru  1598  nic-dfim  1697  nic-dfneg  1698  2nalexn  1856  2nexaln  1858  equvinv  2057  cleljust  2150  sbelx  2287  sb6rfv  2387  cleljustALT  2394  cleljustALT2  2395  dvelimf  2478  sb5rf  2497  sb6rf  2498  sb10f  2557  nexmo  2567  exists2  2687  cleljustab  2742  eqabdv  2894  eqabcri  2904  nne  2960  necon3bbii  3003  necon2abii  3006  necon2bbii  3007  nnel  3072  r19.41v  3193  r3ex  3202  r19.41  3267  rspc2gv  3590  ceqsrexbv  3614  2reu5lem1  3717  2reu5lem2  3718  2reu5lem3  3719  dfsbcq2  3746  cbvreucsf  3896  nss  4000  dfdif3OLD  4072  symdifass  4214  indifdi  4246  difab  4262  neq0  4305  un0  4350  in0  4351  ss0b  4357  2nreu  4408  ralidm  4477  reuprg  4668  snssb  4747  snssg  4748  ssunsn2  4792  iindif2  5042  eqsnuniex  5332  nssss  5436  snopeqop  5489  dffr6  5617  epse  5643  rnep  5917  mptpreima  6239  ralrnmpt  7091  fmptsng  7166  fmptsnd  7167  dff14a  7268  f13dfv  7272  weniso  7352  abnex  7755  uniuni  7760  frpoins3xp3g  8136  xpord3inddlem  8149  eroveu  8809  fsetexb  8860  mapsnend  9032  isfinite2  9257  marypha1lem  9392  marypha2lem4  9397  infcllem  9447  en3lplem2  9581  cantnfp1  9649  scottabf  9865  carden2  9972  fseqenlem1  10007  iscard3  10076  cardnum  10077  alephinit  10078  cardinfima  10080  alephiso  10081  dfac10b  10122  dfackm  10149  isfin5-2  10374  brdom7disj  10514  brdom6disj  10515  fsuppmapnn0fiubex  14027  hash2prb  14508  hashle2prv  14514  hashtpg  14521  hash3tpb  14531  swrdnnn0nd  14693  wrd2ind  14759  s4f1o  14954  cotr2g  15012  relexpindlem  15099  lcmfunsnlem2  16697  ncoprmlnprm  16786  vdwapun  17033  cshwsiun  17158  cshwshash  17163  grpss  19020  symgsubmefmnd  19467  pmtrfrn  19527  pmtrrn2  19529  pmtrprfvalrn  19557  issrg  20269  0ringnnzr  20608  acsfn1p  20881  unocv  21809  dsmmacl  21870  pmatcollpw2lem  22913  fvmptnn04if  22985  toptopon  23053  ordtbas2  23327  ordtrest2  23340  xmeterval  24568  isclmp  25235  ovolfcl  25604  eldv  26036  plyn0mulidp  26421  eltayl  26499  musumsum  27332  2sqreu  27596  2sqreunn  27597  2sqreult  27598  2sqreultb  27599  2sqreunnlt  27600  2sqreunnltb  27601  nosupinfsep  27872  umgrislfupgrlem  29438  numedglnl  29460  ausgrusgrb  29481  cplgr3v  29751  vtxd0nedgb  29804  finsumvtxdg2ssteplem1  29861  isrgr  29875  rgrusgrprc  29905  rgrprcx  29908  upgr2wlk  29982  dfpth2  30044  wwlksnwwlksnon  30230  usgr2wspthon  30283  isclwwlk  30301  clwwlkvbij  30430  iseupthf1o  30519  frcond2  30584  nfrgr2v  30589  4cycl2vnunb  30607  fusgr2wsp2nb  30651  frgrregord013  30712  lejdii  31856  mdslle1i  32635  mdslle2i  32636  mdslj1i  32637  mdslj2i  32638  mo5f  32801  n0nsnel  32827  unipreima  32954  2ndpreima  33019  mgccnv  33285  domnprodeq0  33565  quslsm  33680  mplmonprod  33910  ordtrest2NEW  34279  ordtconnlem1  34280  ballotlem2  34845  bnj115  35080  bnj156  35083  bnj206  35086  bnj110  35212  bnj121  35224  bnj124  35225  bnj130  35228  bnj153  35234  bnj207  35235  bnj581  35262  bnj611  35272  bnj864  35276  bnj865  35277  bnj893  35282  bnj1000  35295  bnj978  35303  bnj1040  35326  bnj1049  35328  bnj1133  35343  bnj1189  35363  satfv1  35809  satfvsucsuc  35811  satfdm  35815  satf0  35818  satf0op  35823  fmlafvel  35831  cnvco1  36205  cnvco2  36206  dfiota3  36367  ss-ax8  36681  trer  36771  nabi1i  36849  nabi2i  36850  regsfromregtco  36993  bj-nnfbit  37327  bj-dvelimdv  37430  bj-gabima  37520  bj-elsngl  37548  bj-nuliotaALT  37638  bj-axseprep  37655  bj-rest10  37674  bj-restuni  37683  con1bii2  37922  con2bii2  37923  topdifinfeq  37940  isbasisrelowllem2  37946  wl-1xor  38072  wl-1mintru1  38078  wl-sb8eut  38177  wl-sb8eutv  38178  inixp  38323  notbinot1  38674  notbinot2  38678  truconj  38696  sbccom2lem  38719  sbccom2  38720  sbccom2f  38721  tsim1  38725  tsxo3  38734  tsxo4  38735  trcoss2  39169  dfcomember3  39354  eqvreldmqs  39355  eqvreldmqs2  39356  dfmembpart2  39468  eldisjn0el  39504  isopos  39900  islvol5  40299  elpadd0  40529  dvhopellsm  41837  diblsmopel  41891  mapdvalc  42349  3factsumint2  42735  3factsumint3  42736  3factsumint4  42737  aks4d1p1p2  42783  aks4d1p7  42796  isprimroot  42806  aks6d1c1p1  42820  aks6d1c2p2  42832  sticksstones22  42881  unitscyglem4  42911  elpwbi  42947  redvmptabs  43067  dffltz  43314  rmxypairf1o  43586  onsupmaxb  43914  ifpnotnotb  44153  ifpdfxor  44161  ifpidg  44165  ifpim123g  44174  ifpim1g  44175  ifpimimb  44178  ifpimim  44183  rp-fakeanorass  44187  elmapintrab  44250  undmrnresiss  44278  clcnvlem  44297  sqrtcvallem1  44305  cnviun  44324  dfxor4  44440  dfhe3  44449  dffrege69  44606  dffrege76  44613  or3or  44697  uneqsn  44699  mnurndlem1  44939  ismnushort  44959  pm10.252  45019  pm10.253  45020  pm10.42  45022  aaanv  45046  pm13.195  45071  pm13.196a  45072  sbc3or  45189  en3lpVD  45501  3orbi123VD  45506  sbc3orgVD  45507  sbcoreleleqVD  45515  undif3VD  45538  ax6e2ndeqVD  45565  ax6e2ndeqALT  45587  sineq0ALT  45593  n0abso  45633  permaxsep  45664  permaxinf2lem  45669  iindif2f  45826  allbutfiinf  46082  limsupequzmptlem  46390  cncfshift  46536  dvnmul  46605  dvnprodlem2  46609  rrxsnicc  46962  sge00  47038  sge0iunmpt  47080  meadjiun  47128  ovolval4lem1  47311  nsssmfmbf  47441  smfmullem4  47456  aibandbiaiffaiffb  47576  plcofph  47626  pldofph  47627  plvcofph  47628  plvcofphax  47629  plvofpos  47630  n0nsn2el  47707  fsetsniunop  47731  2reu8i  47795  aovov0bi  47878  tz6.12-afv2  47922  4an21  47952  ichbi12i  48154  ichnfimlem  48157  spr0nelg  48170  sprvalpwn0  48177  reuprpr  48217  nprmmul1  48221  requad2  48333  clnbgrel  48538  usgrexmpl2nb4  48745  pg4cyclnex  48837  copisnmnd  48879  isprmrng  49046  pgrpgt2nabl  49091  lindslinindsimp2lem5  49187  islininds2  49209  ldepslinc  49234  line2ylem  49476  alsanmo  50533  ralsanmo  50534  alsralrex  50535  2alsraln0id  50541