Theorem bicomd 215

Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.)

Hypothesis

Ref	Expression
bicomd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bicomd	⊢ (𝜑 → (𝜒 ↔ 𝜓))

Proof of Theorem bicomd

Step	Hyp	Ref	Expression
1		bicomd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bicom 214	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 210	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  impbid2  218  syl5ibr  238  ibir  260  bitr2d  272  bitr3d  273  bitr4d  274  syl5rbb  276  syl6rbb  280  con1bid  348  pm5.5  354  imnot  358  baibr  529  rbaib  531  baibd  532  rbaibd  533  anabs5  650  annotanannot  822  pm5.55  931  pm5.54  1000  ninba  1004  pm5.75  1011  sbequ12r  2180  cbvalvOLD  2333  sbal1  2495  eu6OLDOLD  2592  euor2  2646  abbi1dv  2904  necon3bbid  3004  necon4bbid  3008  ralanid  3118  rexanid  3198  ralcom2  3304  gencbvex  3470  sbhypf  3473  alexeqg  3559  clel2g  3566  clel3g  3568  reu8  3638  sbceq2a  3695  sbcco2  3707  reu8nf  3765  2reu4lem  4349  reurexprg  4515  raltpd  4591  ssdifsn  4595  disjxun  4928  opabid  5269  soeq2  5348  posn  5488  xpiindi  5557  fvopab6  6628  cbvfo  6872  f1eqcocnv  6884  isoid  6907  isoini  6916  isosolem  6925  riotaeqimp  6962  resoprab2  7089  tfisi  7391  tfinds2  7396  f1oweALT  7487  dfoprab3  7562  opiota  7567  mpocurryd  7740  oalimcl  7989  omword  7999  oeword  8019  nnacan  8057  nnmcan  8063  mapsnd  8250  findcard2s  8556  funisfsupp  8635  suppeqfsuppbi  8644  eqinf  8745  inflb  8750  infglb  8751  infglbb  8752  infltoreq  8763  infempty  8768  brwdomn0  8830  cantnfp1lem3  8939  ssrankr1  9060  r1pw  9070  djulf1o  9137  djurf1o  9138  aleph11  9306  alephval3  9332  gch-kn  9899  wunex2  9960  lttri2  10525  wloglei  10975  divne0b  11112  lemul1  11295  nnnle0  11476  div4p1lem1div2  11705  nn0ind-raph  11898  zindd  11899  suprfinzcl  11913  rebtwnz  12164  qreccl  12186  elpq  12192  xrlttri2  12355  2resupmax  12401  xmulneg1  12481  iooshf  12634  difreicc  12689  fzofzim  12902  elfzomelpfzo  12959  elfznelfzo  12960  zmodid2  13085  2submod  13118  modfzo0difsn  13129  om2uzlti  13136  expcan  13351  hashvnfin  13539  hashneq0  13543  prhash2ex  13576  hashgt0elex  13578  hashgt12el  13599  hashgt12el2  13600  hashbclem  13626  hashf1lem2  13630  prprrab  13645  swrdn0OLD  13823  swrd0  13829  2swrdeqwrdeqOLD  13849  pfxn0  13871  pfxsuffeqwrdeq  13883  swrdswrd  13890  pfxccat3  13939  swrdccat3OLD  13940  repswswrd  14006  cshf1  14037  cshw1repsw  14050  relexpindlem  14286  absz  14535  iserex  14877  prodrb  15149  absdvdsb  15491  dvdsabsb  15492  modmulconst  15504  dvdsadd  15515  dvdsabseq  15526  mod2eq0even  15558  oddnn02np1  15560  oddge22np1  15561  evennn02n  15562  evennn2n  15563  zeo5  15568  sadadd2lem2  15662  smupvallem  15695  gcdass  15754  lcmdvds  15811  lcmass  15817  divgcdcoprm0  15868  divgcdcoprmex  15869  1nprm  15882  dvdsnprmd  15893  ncoprmlnprm  15927  isevengcd2  15929  m1dvdsndvds  15994  cshws0  16294  sbcie2s  16399  sbcie3s  16400  dfiso2  16903  initoid  17126  termoid  17127  funcestrcsetclem8  17258  lublecllem  17459  odudlatb  17667  issubm2  17819  mgm2nsgrplem2  17878  nsgacs  18102  cycsubg2  18103  gapm  18210  sscntz  18230  pgrpsubgsymgbi  18299  f1omvdcnv  18336  pmtrprfvalrn  18380  odval2  18444  lsmcntz  18566  rhmf1o  19210  isrim  19211  snifpsrbag  19863  gsumply1eq  20179  dfprm2  20346  psgnfix2  20448  islinds3  20683  islindf4  20687  mdetdiaglem  20914  mdetunilem9  20936  slesolinv  20996  slesolex  20998  cpmatel2  21028  m2cpmghm  21059  m2cpminvid2  21070  pm2mpf1  21114  chfacfscmul0  21173  chfacfscmulfsupp  21174  chfacfpmmul0  21177  chfacfpmmulfsupp  21178  isopn2  21347  cmpsub  21715  connsub  21736  ncvs1  23467  rrxmvallem  23713  itg1mulc  24011  lhop1  24317  mdegleb  24364  lawcos  25098  leibpi  25225  2lgslem1a  25672  2sq2  25714  iscgra  26300  colinearalg  26402  edg0iedg0  26546  uhgreq12g  26556  uhgrvtxedgiedgb  26627  usgredg2v  26715  edg0usgr  26741  dfnbgr2  26825  nbuhgr  26831  nbusgredgeu0  26856  nb3grprlem1  26868  nb3grpr  26870  uvtx2vtx1edgb  26887  wlkeq  27121  redwlk  27163  uhgrwkspthlem2  27246  usgr2wlkspth  27251  pthdlem1  27258  cyclnspth  27292  crctcshwlkn0lem1  27299  crctcshwlkn0lem4  27302  crctcsh  27313  iswwlksnx  27329  wwlksm1edg  27370  wwlksm1edgOLD  27371  wwlksnextsurj  27394  wwlksnextsurOLD  27399  wwlksnextproplem3  27416  wwlksnextproplem3OLD  27417  2wlkdlem4  27437  2wlkdlem5  27438  2pthdlem1  27439  s3wwlks2on  27465  wpthswwlks2on  27470  elwspths2spth  27476  rusgrnumwwlks  27483  rusgrnumwwlksOLD  27484  umgrclwwlkge2  27500  clwlkclwwlklem2a4  27506  clwlkclwwlk  27511  clwlkclwwlkOLD  27512  clwlkclwwlkflem  27515  clwwisshclwws  27533  isclwwlknx  27554  clwwlknwwlksnb  27581  eclclwwlkn1  27602  clwwlknonel  27626  clwwlknun  27643  3wlkdlem6  27697  frgrncvvdeqlem9  27844  fusgreg2wsp  27873  numclwwlk2lem1lem  27879  extwwlkfab  27894  extwwlkfabOLD  27895  frgrreggt1  27953  ubthlem1  28428  norm-i  28688  hoeq  29321  nmopgt0  29473  pjimai  29737  chirredi  29955  addltmulALT  30007  opreu2reuALT  30025  sbcies  30036  iunrdx  30087  disjrdx  30110  cnvoprabOLD  30211  archiabl  30493  oms0  31200  eulerpartgbij  31275  sgnneg  31444  sgn3da  31445  reprinrn  31537  satf0op  32187  mrsubrn  32280  sotrine  32523  etasslt  32795  topfne  33223  unbdqndv1  33367  bj-hbntbi  33548  bj-abbi1dv  33612  bj-issetwt  33682  dfgcd3  34047  topdifinfeq  34073  wl-sb6rft  34226  wl-sbalnae  34239  wl-dfralf  34280  sin2h  34323  poimirlem16  34349  poimirlem17  34350  poimirlem25  34358  mbfresfi  34379  itg2addnclem  34384  itg2addnclem2  34385  itg2addnclem3  34386  ftc1anclem1  34408  isidlc  34735  islshpsm  35561  lshpkrlem1  35691  opcon1b  35779  lautlt  36672  lauteq  36676  idlaut  36677  diblsmopel  37752  doch11  37954  rabeqcda  38550  prjsprellsp  38668  prjspeclsp  38669  istopclsd  38692  eqrabdioph  38770  rexzrexnn0  38797  zindbi  38939  expdiophlem2  39015  inintabd  39301  cnvcnvintabd  39322  cnvintabd  39325  fsovrfovd  39718  ntrclsiso  39780  ntrneifv3  39795  ntrneineine0lem  39796  ntrneicls11  39803  suprleubrd  39881  suprlubrd  39885  lemuldiv4d  39888  pm14.122a  40171  3impexpbicomi  40233  onfrALTlem5  40295  bitr3VD  40602  onfrALTlem5VD  40638  csbrngVD  40649  pwpwuni  40739  supxrre3  41023  xrralrecnnge  41093  eliooshift  41214  limsupre2lem  41437  liminflimsupclim  41520  xlimbr  41540  smfrec  42496  reuf1odnf  42713  2reuimp  42721  ralbinrald  42728  afvco2  42782  dfatdmfcoafv2  42860  recnmulnred  42912  sqrtnegnre  42914  subsubelfzo0  42933  ichcircshi  42983  sprvalpwle2  43020  sprsymrelf1lem  43022  sbcpr  43052  poprelb  43055  31prm  43129  requad01  43155  dfeven3  43192  iseven5  43198  0noddALTV  43223  2noddALTV  43227  fpprmod  43261  sbgoldbaltlem1  43313  bgoldbtbndlem2  43340  isomuspgrlem2d  43365  0nodd  43446  2nodd  43448  isassintop  43482  rnghmf1o  43539  isrngim  43540  uzlidlring  43565  funcringcsetcALTV2lem8  43679  funcringcsetclem8ALTV  43702  nn0sumltlt  43763  ply1mulgsumlem2  43809  islindeps  43876  lindslinindsimp1  43880  lindslinindsimp2  43886  snlindsntor  43894  zlmodzxznm  43920  ldepslinc  43932  difmodm1lt  43951  elbigo2  43981  elbigolo1  43986  logblt1b  43993  fldivexpfllog2  43994  nnolog2flm1  44019  digexp  44036  nn0sumshdiglemB  44049  itsclquadeu  44133  itscnhlinecirc02p  44141