Theorem bicomd 223

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 222	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 218	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ 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:  impbid2  226  imbitrrid  246  ibir  268  bitr2d  280  bitr3d  281  bitr4d  282  bitr2id  284  bitr2di  288  con1bid  355  pm5.5  361  imnot  365  baibr  536  rbaib  538  baibd  539  anabs5  663  annotanannot  834  pm5.55  950  pm5.54  1019  ninba  1023  pm5.75  1030  sbequ12r  2253  sbal1  2533  euor2  2613  eqabcdv  2870  necon3bbid  2970  necon4bbid  2974  ralanid  3085  rexanid  3086  sbralieALT  3337  ralcom2  3361  rmoanid  3374  reuanid  3375  rabrabi  3440  gencbvex  3525  sbhypfOLD  3529  alexeqg  3635  clel2g  3643  clel3g  3645  clel4g  3647  reurab  3689  reu8  3721  sbceq2a  3782  sbcco2  3797  reu8nf  3857  notabw  4293  2reu4lem  4502  reurexprg  4685  raltpd  4762  ssdifsn  4769  uniprg  4904  disjxun  5122  opabidw  5504  opabid  5505  soeq2  5588  sotrine  5606  posn  5745  xpiindi  5820  dmopab2rex  5902  elpredg  6309  fvopab6  7025  cbvfo  7287  f1eqcocnv  7299  isoid  7327  isoini  7336  isosolem  7345  riotaeqimp  7393  riotarab  7409  resoprab2  7531  tfisi  7859  tfinds2  7864  f1oweALT  7976  dfoprab3  8058  opiota  8063  xpord2indlem  8151  xpord3inddlem  8158  mpocurryd  8273  oalimcl  8577  omword  8587  oeword  8607  nnacan  8645  nnmcan  8651  mapsnd  8905  findcard2s  9184  funisfsupp  9384  suppeqfsuppbi  9396  eqinf  9502  inflb  9507  infglb  9508  infglbb  9509  infltoreq  9521  infempty  9526  brwdomn0  9588  cantnfp1lem3  9699  ssrankr1  9854  r1pw  9864  djulf1o  9931  djurf1o  9932  aleph11  10103  alephval3  10129  gch-kn  10696  wunex2  10757  lttri2  11322  wloglei  11774  divne0b  11912  lemul1  12098  nnnle0  12278  div4p1lem1div2  12501  nn0ind-raph  12698  zindd  12699  suprfinzcl  12712  rebtwnz  12968  qreccl  12990  elpq  12996  xrlttri2  13163  2resupmax  13209  xmulneg1  13290  iooshf  13448  difreicc  13506  fzofzim  13731  elfzomelpfzo  13792  elfznelfzo  13793  zmodid2  13921  2submod  13955  modfzo0difsn  13966  om2uzlti  13973  expcan  14192  hashvnfin  14383  hashneq0  14387  prhash2ex  14422  hashgt0elex  14424  hashgt12el  14445  hashgt12el2  14446  hashbclem  14475  hashf1lem2  14479  prprrab  14496  swrd0  14681  pfxn0  14709  swrdswrd  14728  pfxccat3  14757  repswswrd  14807  cshf1  14833  cshw1repsw  14846  relexpindlem  15087  absz  15335  iserex  15678  prodrb  15953  absdvdsb  16299  dvdsabsb  16300  modmulconst  16312  dvdsadd  16326  dvdsabseq  16337  mod2eq0even  16370  oddnn02np1  16372  oddge22np1  16373  evennn02n  16374  evennn2n  16375  zeo5  16380  sadadd2lem2  16474  smupvallem  16507  gcdass  16571  lcmdvds  16632  lcmass  16638  divgcdcoprm0  16689  divgcdcoprmex  16690  1nprm  16703  dvdsnprmd  16714  prmdvdssq  16742  ncoprmlnprm  16752  isevengcd2  16754  m1dvdsndvds  16823  cshws0  17126  sbcie3s  17186  dfiso2  17790  initoid  18019  termoid  18020  funcestrcsetclem8  18164  lublecllem  18375  odudlatb  18540  sgrppropd  18714  issubm2  18787  mgm2nsgrplem2  18902  nsgacs  19150  cycsubg2  19198  gapm  19294  sscntz  19314  pgrpsubgsymgbi  19394  f1omvdcnv  19430  pmtrprfvalrn  19474  odval2  19537  lsmcntz  19665  rngpropd  20139  rnghmf1o  20417  isrngim2  20418  rhmf1o  20456  isrim  20457  isrimOLD  20458  dfprm2  21439  pzriprnglem10  21456  psgnfix2  21564  islinds3  21799  islindf4  21803  snifpsrbag  21885  gsumply1eq  22252  mdetdiaglem  22541  mdetunilem9  22563  slesolinv  22623  slesolex  22625  cpmatel2  22656  m2cpmghm  22687  m2cpminvid2  22698  pm2mpf1  22742  chfacfscmul0  22801  chfacfscmulfsupp  22802  chfacfpmmul0  22805  chfacfpmmulfsupp  22806  isopn2  22975  cmpsub  23343  connsub  23364  ncvs1  25114  rrxmvallem  25361  itg1mulc  25662  lhop1  25976  mdegleb  26026  lawcos  26783  leibpi  26909  2lgslem1a  27359  2sq2  27401  sletric  27733  bdayon  28230  n0subs2  28311  0reno  28405  colinearalg  28894  edg0iedg0  29039  uhgreq12g  29049  uhgrvtxedgiedgb  29120  usgredg2v  29211  edg0usgr  29237  dfnbgr2  29321  nbuhgr  29327  nbusgredgeu0  29352  nb3grprlem1  29364  nb3grpr  29366  uvtx2vtx1edgb  29383  redwlk  29657  uhgrwkspthlem2  29741  usgr2wlkspth  29746  pthdlem1  29753  cyclnspth  29788  crctcshwlkn0lem1  29797  crctcshwlkn0lem4  29800  crctcsh  29811  iswwlksnx  29827  wwlksm1edg  29868  wwlksnextsurj  29887  wwlksnextproplem3  29898  2wlkdlem4  29915  2wlkdlem5  29916  2pthdlem1  29917  s3wwlks2on  29943  wpthswwlks2on  29948  elwspths2spth  29954  rusgrnumwwlks  29961  umgrclwwlkge2  29977  clwlkclwwlklem2a4  29983  clwlkclwwlk  29988  clwlkclwwlkflem  29990  clwwisshclwws  30001  isclwwlknx  30022  clwwlknwwlksnb  30041  eclclwwlkn1  30061  clwwlknonel  30081  clwwlknun  30098  3wlkdlem6  30151  frgrncvvdeqlem9  30293  fusgreg2wsp  30322  numclwwlk2lem1lem  30328  extwwlkfab  30338  frgrreggt1  30379  ubthlem1  30856  norm-i  31115  hoeq  31746  nmopgt0  31898  pjimai  32162  chirredi  32380  addltmulALT  32432  bian1d  32442  opreu2reuALT  32463  sbcies  32474  rmounid  32481  iunrdx  32549  disjrdx  32577  sgnneg  32817  sgn3da  32818  archiabl  33201  islbs5  33400  ist0cld  33869  oms0  34334  eulerpartgbij  34409  reprinrn  34655  usgrgt2cycl  35157  satfv1lem  35389  satf0op  35404  dmopab3rexdif  35432  satefvfmla0  35445  mrsubrn  35540  topfne  36377  unbdqndv1  36531  bj-hbntbi  36727  bj-issetwt  36898  bj-clel3gALT  37071  copsex2d  37162  bj-elid6  37193  dfgcd3  37347  topdifinfeq  37373  wl-sbalnae  37585  sin2h  37639  poimirlem16  37665  poimirlem17  37666  poimirlem25  37674  mbfresfi  37695  itg2addnclem  37700  itg2addnclem2  37701  itg2addnclem3  37702  ftc1anclem1  37722  isidlc  38044  eldmressnALTV  38295  islshpsm  39003  lshpkrlem1  39133  opcon1b  39221  lautlt  40115  lauteq  40119  idlaut  40120  diblsmopel  41195  doch11  41397  recbothd  42010  aks4d1p8d2  42103  aks4d1p8  42105  isprimroot2  42112  posbezout  42118  aks6d1c5lem1  42154  sticksstones1  42164  sticksstones11  42174  sticksstones22  42186  aks6d1c6lem3  42190  aks6d1c6lem4  42191  aks6d1c7  42202  aks5lem8  42219  f1o2d2  42251  dvdsexpnn0  42352  redvmptabs  42378  prjsprellsp  42609  prjspeclsp  42610  abbibw  42675  istopclsd  42698  eqrabdioph  42775  rexzrexnn0  42802  zindbi  42945  expdiophlem2  43021  onsupeqmax  43245  onsupeqnmax  43246  ordeldif  43257  infordmin  43531  inintabd  43578  cnvcnvintabd  43599  cnvintabd  43602  sqrtcvallem1  43630  reabsifneg  43631  fsovrfovd  44008  ntrclsiso  44066  ntrneifv3  44081  ntrneineine0lem  44082  ntrneicls11  44089  suprleubrd  44165  suprlubrd  44167  lemuldiv4d  44170  pm14.122a  44421  3impexpbicomi  44481  onfrALTlem5  44542  bitr3VD  44848  onfrALTlem5VD  44884  csbrngVD  44895  pwpwuni  45061  supxrre3  45332  xrralrecnnge  45397  eliooshift  45515  limsupre2lem  45733  liminflimsupclim  45816  xlimbr  45836  smfrec  46798  fsetprcnexALT  47071  f1cof1b  47086  reuf1odnf  47116  2reuimp  47124  ralbinrald  47131  afvco2  47185  dfatdmfcoafv2  47263  recnmulnred  47314  sqrtnegnre  47316  subsubelfzo0  47335  ceilbi  47342  ichcircshi  47448  sprvalpwle2  47483  sprsymrelf1lem  47485  sbcpr  47515  poprelb  47518  31prm  47591  requad01  47615  dfeven3  47652  iseven5  47658  0noddALTV  47683  2noddALTV  47687  fpprmod  47721  sbgoldbaltlem1  47773  bgoldbtbndlem2  47800  dfclnbgr2  47817  dfsclnbgr2  47839  dfvopnbgr2  47846  dfsclnbgr6  47851  isuspgrim0lem  47886  usgrgrtrirex  47942  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  0nodd  48125  2nodd  48127  isassintop  48165  uzlidlring  48190  funcringcsetcALTV2lem8  48252  funcringcsetclem8ALTV  48275  nn0sumltlt  48305  ply1mulgsumlem2  48343  islindeps  48409  lindslinindsimp1  48413  lindslinindsimp2  48419  snlindsntor  48427  zlmodzxznm  48453  ldepslinc  48465  difmodm1lt  48482  elbigo2  48512  elbigolo1  48517  logblt1b  48524  fldivexpfllog2  48525  nnolog2flm1  48550  digexp  48567  nn0sumshdiglemB  48580  itsclquadeu  48737  itscnhlinecirc02p  48745  ipolublem  48940  ipoglblem  48943