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  664  annotanannot  835  pm5.55  951  pm5.54  1020  ninba  1024  pm5.75  1031  sbequ12r  2260  sbal1  2533  euor2  2614  eqabcdv  2871  necon3bbid  2970  necon4bbid  2974  ralanid  3086  rexanid  3087  sbralieALT  3325  ralcom2  3349  rmoanid  3362  reuanid  3363  rabrabi  3420  gencbvex  3501  alexeqg  3607  clel2g  3615  clel3g  3617  clel4g  3619  reurab  3661  reu8  3693  sbceq2a  3754  sbcco2  3769  reu8nf  3829  notabw  4267  2reu4lem  4478  reurexprg  4663  raltpd  4740  ssdifsn  4746  uniprg  4881  disjxun  5098  opabidw  5480  opabid  5481  soeq2  5562  sotrine  5580  posn  5718  xpiindi  5792  dmopab2rex  5874  elpredg  6281  fvopab6  6984  cbvfo  7245  f1eqcocnv  7257  isoid  7285  isoini  7294  isosolem  7303  riotaeqimp  7351  riotarab  7367  resoprab2  7487  tfisi  7811  tfinds2  7816  f1oweALT  7926  dfoprab3  8008  opiota  8013  xpord2indlem  8099  xpord3inddlem  8106  mpocurryd  8221  oalimcl  8497  omword  8507  oeword  8528  nnacan  8566  nnmcan  8572  mapsnd  8836  findcard2s  9102  funisfsupp  9282  suppeqfsuppbi  9294  eqinf  9400  inflb  9405  infglb  9406  infglbb  9407  infltoreq  9419  infempty  9424  brwdomn0  9486  cantnfp1lem3  9601  ssrankr1  9759  r1pw  9769  djulf1o  9836  djurf1o  9837  aleph11  10006  alephval3  10032  gch-kn  10600  wunex2  10661  lttri2  11227  wloglei  11681  divne0b  11819  lemul1  12005  nnnle0  12190  div4p1lem1div2  12408  nn0ind-raph  12604  zindd  12605  suprfinzcl  12618  rebtwnz  12872  qreccl  12894  elpq  12900  xrlttri2  13068  2resupmax  13115  xmulneg1  13196  iooshf  13354  difreicc  13412  fzofzim  13637  elfzomelpfzo  13700  elfznelfzo  13701  zmodid2  13831  2submod  13867  modfzo0difsn  13878  om2uzlti  13885  expcan  14104  hashvnfin  14295  hashneq0  14299  prhash2ex  14334  hashgt0elex  14336  hashgt12el  14357  hashgt12el2  14358  hashbclem  14387  hashf1lem2  14391  prprrab  14408  swrd0  14594  pfxn0  14622  swrdswrd  14640  pfxccat3  14669  repswswrd  14719  cshf1  14745  cshw1repsw  14758  relexpindlem  14998  absz  15246  iserex  15592  prodrb  15867  absdvdsb  16213  dvdsabsb  16214  modmulconst  16227  dvdsadd  16241  dvdsabseq  16252  mod2eq0even  16285  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  zeo5  16295  sadadd2lem2  16389  smupvallem  16422  gcdass  16486  lcmdvds  16547  lcmass  16553  divgcdcoprm0  16604  divgcdcoprmex  16605  1nprm  16618  dvdsnprmd  16629  prmdvdssq  16657  ncoprmlnprm  16667  isevengcd2  16669  m1dvdsndvds  16738  cshws0  17041  sbcie3s  17101  dfiso2  17708  initoid  17937  termoid  17938  funcestrcsetclem8  18082  lublecllem  18293  odudlatb  18460  sgrppropd  18668  issubm2  18741  mgm2nsgrplem2  18856  nsgacs  19103  cycsubg2  19151  gapm  19247  sscntz  19267  pgrpsubgsymgbi  19349  f1omvdcnv  19385  pmtrprfvalrn  19429  odval2  19492  lsmcntz  19620  rngpropd  20121  rnghmf1o  20400  isrngim2  20401  rhmf1o  20438  isrim  20439  dfprm2  21440  pzriprnglem10  21457  psgnfix2  21566  islinds3  21801  islindf4  21805  snifpsrbag  21888  gsumply1eq  22265  mdetdiaglem  22554  mdetunilem9  22576  slesolinv  22636  slesolex  22638  cpmatel2  22669  m2cpmghm  22700  m2cpminvid2  22711  pm2mpf1  22755  chfacfscmul0  22814  chfacfscmulfsupp  22815  chfacfpmmul0  22818  chfacfpmmulfsupp  22819  isopn2  22988  cmpsub  23356  connsub  23377  ncvs1  25125  rrxmvallem  25372  itg1mulc  25673  lhop1  25987  mdegleb  26037  lawcos  26794  leibpi  26920  2lgslem1a  27370  2sq2  27412  lestric  27748  bdayons  28284  n0subs2  28372  bdaypw2n0bndlem  28471  colinearalg  28995  edg0iedg0  29140  uhgreq12g  29150  uhgrvtxedgiedgb  29221  usgredg2v  29312  edg0usgr  29338  dfnbgr2  29422  nbuhgr  29428  nbusgredgeu0  29453  nb3grprlem1  29465  nb3grpr  29467  uvtx2vtx1edgb  29484  redwlk  29756  uhgrwkspthlem2  29839  usgr2wlkspth  29844  pthdlem1  29851  cyclnspth  29886  crctcshwlkn0lem1  29895  crctcshwlkn0lem4  29898  crctcsh  29909  iswwlksnx  29925  wwlksm1edg  29966  wwlksnextsurj  29985  wwlksnextproplem3  29996  2wlkdlem4  30013  2wlkdlem5  30014  2pthdlem1  30015  s3wwlks2on  30041  sps3wwlks2on  30042  wpthswwlks2on  30049  elwspths2spth  30055  rusgrnumwwlks  30062  umgrclwwlkge2  30078  clwlkclwwlklem2a4  30084  clwlkclwwlk  30089  clwlkclwwlkflem  30091  clwwisshclwws  30102  isclwwlknx  30123  clwwlknwwlksnb  30142  eclclwwlkn1  30162  clwwlknonel  30182  clwwlknun  30199  3wlkdlem6  30252  frgrncvvdeqlem9  30394  fusgreg2wsp  30423  numclwwlk2lem1lem  30429  extwwlkfab  30439  frgrreggt1  30480  ubthlem1  30958  norm-i  31217  hoeq  31848  nmopgt0  32000  pjimai  32264  chirredi  32482  addltmulALT  32534  opreu2reuALT  32563  sbcies  32574  rmounid  32581  iunrdx  32650  disjrdx  32678  sgnneg  32925  sgn3da  32926  archiabl  33292  islbs5  33473  ist0cld  34011  oms0  34475  eulerpartgbij  34550  reprinrn  34796  usgrgt2cycl  35346  satfv1lem  35578  satf0op  35593  dmopab3rexdif  35621  satefvfmla0  35634  mrsubrn  35729  topfne  36570  unbdqndv1  36730  bj-hbntbi  36949  bj-issetwt  37123  bj-clel3gALT  37296  copsex2d  37394  bj-elid6  37425  dfgcd3  37579  topdifinfeq  37605  wl-sbalnae  37817  sin2h  37861  poimirlem16  37887  poimirlem17  37888  poimirlem25  37896  mbfresfi  37917  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  ftc1anclem1  37944  isidlc  38266  eldmressnALTV  38530  islshpsm  39356  lshpkrlem1  39486  opcon1b  39574  lautlt  40467  lauteq  40471  idlaut  40472  diblsmopel  41547  doch11  41749  recbothd  42362  aks4d1p8d2  42455  aks4d1p8  42457  isprimroot2  42464  posbezout  42470  aks6d1c5lem1  42506  sticksstones1  42516  sticksstones11  42526  sticksstones22  42538  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c7  42554  aks5lem8  42571  f1o2d2  42605  dvdsexpnn0  42704  redvmptabs  42730  prjsprellsp  42969  prjspeclsp  42970  abbibw  43035  istopclsd  43057  eqrabdioph  43134  rexzrexnn0  43161  zindbi  43303  expdiophlem2  43379  onsupeqmax  43603  onsupeqnmax  43604  ordeldif  43615  infordmin  43888  inintabd  43935  cnvcnvintabd  43956  cnvintabd  43959  sqrtcvallem1  43987  reabsifneg  43988  fsovrfovd  44365  ntrclsiso  44423  ntrneifv3  44438  ntrneineine0lem  44439  ntrneicls11  44446  suprleubrd  44522  suprlubrd  44524  lemuldiv4d  44527  pm14.122a  44778  3impexpbicomi  44837  onfrALTlem5  44898  bitr3VD  45204  onfrALTlem5VD  45240  csbrngVD  45251  pwpwuni  45417  supxrre3  45684  xrralrecnnge  45748  eliooshift  45866  limsupre2lem  46082  liminflimsupclim  46165  xlimbr  46185  smfrec  47147  fsetprcnexALT  47422  f1cof1b  47437  reuf1odnf  47467  2reuimp  47475  ralbinrald  47482  afvco2  47536  dfatdmfcoafv2  47614  recnmulnred  47665  sqrtnegnre  47667  subsubelfzo0  47686  ceilbi  47693  ichcircshi  47814  sprvalpwle2  47849  sprsymrelf1lem  47851  sbcpr  47881  poprelb  47884  31prm  47957  requad01  47981  dfeven3  48018  iseven5  48024  0noddALTV  48049  2noddALTV  48053  fpprmod  48087  sbgoldbaltlem1  48139  bgoldbtbndlem2  48166  dfclnbgr2  48183  dfsclnbgr2  48206  dfvopnbgr2  48213  dfsclnbgr6  48218  isuspgrim0lem  48253  usgrgrtrirex  48310  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgn4cyclex  48486  0nodd  48530  2nodd  48532  isassintop  48570  uzlidlring  48595  funcringcsetcALTV2lem8  48657  funcringcsetclem8ALTV  48680  nn0sumltlt  48710  ply1mulgsumlem2  48747  islindeps  48813  lindslinindsimp1  48817  lindslinindsimp2  48823  snlindsntor  48831  zlmodzxznm  48857  ldepslinc  48869  elbigo2  48912  elbigolo1  48917  logblt1b  48924  fldivexpfllog2  48925  nnolog2flm1  48950  digexp  48967  nn0sumshdiglemB  48980  itsclquadeu  49137  itscnhlinecirc02p  49145  ipolublem  49345  ipoglblem  49348