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  2259  sbal1  2532  euor2  2613  eqabcdv  2870  necon3bbid  2969  necon4bbid  2973  ralanid  3084  rexanid  3085  sbralieALT  3323  ralcom2  3347  rmoanid  3360  reuanid  3361  rabrabi  3418  gencbvex  3499  alexeqg  3605  clel2g  3613  clel3g  3615  clel4g  3617  reurab  3659  reu8  3691  sbceq2a  3752  sbcco2  3767  reu8nf  3827  notabw  4265  2reu4lem  4476  reurexprg  4661  raltpd  4738  ssdifsn  4744  uniprg  4879  disjxun  5096  opabidw  5472  opabid  5473  soeq2  5554  sotrine  5572  posn  5710  xpiindi  5784  dmopab2rex  5866  elpredg  6273  fvopab6  6975  cbvfo  7235  f1eqcocnv  7247  isoid  7275  isoini  7284  isosolem  7293  riotaeqimp  7341  riotarab  7357  resoprab2  7477  tfisi  7801  tfinds2  7806  f1oweALT  7916  dfoprab3  7998  opiota  8003  xpord2indlem  8089  xpord3inddlem  8096  mpocurryd  8211  oalimcl  8487  omword  8497  oeword  8518  nnacan  8556  nnmcan  8562  mapsnd  8824  findcard2s  9090  funisfsupp  9270  suppeqfsuppbi  9282  eqinf  9388  inflb  9393  infglb  9394  infglbb  9395  infltoreq  9407  infempty  9412  brwdomn0  9474  cantnfp1lem3  9589  ssrankr1  9747  r1pw  9757  djulf1o  9824  djurf1o  9825  aleph11  9994  alephval3  10020  gch-kn  10588  wunex2  10649  lttri2  11215  wloglei  11669  divne0b  11807  lemul1  11993  nnnle0  12178  div4p1lem1div2  12396  nn0ind-raph  12592  zindd  12593  suprfinzcl  12606  rebtwnz  12860  qreccl  12882  elpq  12888  xrlttri2  13056  2resupmax  13103  xmulneg1  13184  iooshf  13342  difreicc  13400  fzofzim  13625  elfzomelpfzo  13688  elfznelfzo  13689  zmodid2  13819  2submod  13855  modfzo0difsn  13866  om2uzlti  13873  expcan  14092  hashvnfin  14283  hashneq0  14287  prhash2ex  14322  hashgt0elex  14324  hashgt12el  14345  hashgt12el2  14346  hashbclem  14375  hashf1lem2  14379  prprrab  14396  swrd0  14582  pfxn0  14610  swrdswrd  14628  pfxccat3  14657  repswswrd  14707  cshf1  14733  cshw1repsw  14746  relexpindlem  14986  absz  15234  iserex  15580  prodrb  15855  absdvdsb  16201  dvdsabsb  16202  modmulconst  16215  dvdsadd  16229  dvdsabseq  16240  mod2eq0even  16273  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  zeo5  16283  sadadd2lem2  16377  smupvallem  16410  gcdass  16474  lcmdvds  16535  lcmass  16541  divgcdcoprm0  16592  divgcdcoprmex  16593  1nprm  16606  dvdsnprmd  16617  prmdvdssq  16645  ncoprmlnprm  16655  isevengcd2  16657  m1dvdsndvds  16726  cshws0  17029  sbcie3s  17089  dfiso2  17696  initoid  17925  termoid  17926  funcestrcsetclem8  18070  lublecllem  18281  odudlatb  18448  sgrppropd  18656  issubm2  18729  mgm2nsgrplem2  18844  nsgacs  19091  cycsubg2  19139  gapm  19235  sscntz  19255  pgrpsubgsymgbi  19337  f1omvdcnv  19373  pmtrprfvalrn  19417  odval2  19480  lsmcntz  19608  rngpropd  20109  rnghmf1o  20388  isrngim2  20389  rhmf1o  20426  isrim  20427  dfprm2  21428  pzriprnglem10  21445  psgnfix2  21554  islinds3  21789  islindf4  21793  snifpsrbag  21876  gsumply1eq  22253  mdetdiaglem  22542  mdetunilem9  22564  slesolinv  22624  slesolex  22626  cpmatel2  22657  m2cpmghm  22688  m2cpminvid2  22699  pm2mpf1  22743  chfacfscmul0  22802  chfacfscmulfsupp  22803  chfacfpmmul0  22806  chfacfpmmulfsupp  22807  isopn2  22976  cmpsub  23344  connsub  23365  ncvs1  25113  rrxmvallem  25360  itg1mulc  25661  lhop1  25975  mdegleb  26025  lawcos  26782  leibpi  26908  2lgslem1a  27358  2sq2  27400  lestric  27736  bdayons  28272  n0subs2  28360  bdaypw2n0bndlem  28459  colinearalg  28983  edg0iedg0  29128  uhgreq12g  29138  uhgrvtxedgiedgb  29209  usgredg2v  29300  edg0usgr  29326  dfnbgr2  29410  nbuhgr  29416  nbusgredgeu0  29441  nb3grprlem1  29453  nb3grpr  29455  uvtx2vtx1edgb  29472  redwlk  29744  uhgrwkspthlem2  29827  usgr2wlkspth  29832  pthdlem1  29839  cyclnspth  29874  crctcshwlkn0lem1  29883  crctcshwlkn0lem4  29886  crctcsh  29897  iswwlksnx  29913  wwlksm1edg  29954  wwlksnextsurj  29973  wwlksnextproplem3  29984  2wlkdlem4  30001  2wlkdlem5  30002  2pthdlem1  30003  s3wwlks2on  30029  sps3wwlks2on  30030  wpthswwlks2on  30037  elwspths2spth  30043  rusgrnumwwlks  30050  umgrclwwlkge2  30066  clwlkclwwlklem2a4  30072  clwlkclwwlk  30077  clwlkclwwlkflem  30079  clwwisshclwws  30090  isclwwlknx  30111  clwwlknwwlksnb  30130  eclclwwlkn1  30150  clwwlknonel  30170  clwwlknun  30187  3wlkdlem6  30240  frgrncvvdeqlem9  30382  fusgreg2wsp  30411  numclwwlk2lem1lem  30417  extwwlkfab  30427  frgrreggt1  30468  ubthlem1  30945  norm-i  31204  hoeq  31835  nmopgt0  31987  pjimai  32251  chirredi  32469  addltmulALT  32521  bian1d  32530  opreu2reuALT  32551  sbcies  32562  rmounid  32569  iunrdx  32638  disjrdx  32666  sgnneg  32914  sgn3da  32915  archiabl  33280  islbs5  33461  ist0cld  33990  oms0  34454  eulerpartgbij  34529  reprinrn  34775  usgrgt2cycl  35324  satfv1lem  35556  satf0op  35571  dmopab3rexdif  35599  satefvfmla0  35612  mrsubrn  35707  topfne  36548  unbdqndv1  36708  bj-hbntbi  36905  bj-issetwt  37076  bj-clel3gALT  37249  copsex2d  37344  bj-elid6  37375  dfgcd3  37529  topdifinfeq  37555  wl-sbalnae  37767  sin2h  37811  poimirlem16  37837  poimirlem17  37838  poimirlem25  37846  mbfresfi  37867  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  ftc1anclem1  37894  isidlc  38216  eldmressnALTV  38474  islshpsm  39250  lshpkrlem1  39380  opcon1b  39468  lautlt  40361  lauteq  40365  idlaut  40366  diblsmopel  41441  doch11  41643  recbothd  42256  aks4d1p8d2  42349  aks4d1p8  42351  isprimroot2  42358  posbezout  42364  aks6d1c5lem1  42400  sticksstones1  42410  sticksstones11  42420  sticksstones22  42432  aks6d1c6lem3  42436  aks6d1c6lem4  42437  aks6d1c7  42448  aks5lem8  42465  f1o2d2  42499  dvdsexpnn0  42599  redvmptabs  42625  prjsprellsp  42864  prjspeclsp  42865  abbibw  42930  istopclsd  42952  eqrabdioph  43029  rexzrexnn0  43056  zindbi  43198  expdiophlem2  43274  onsupeqmax  43498  onsupeqnmax  43499  ordeldif  43510  infordmin  43783  inintabd  43830  cnvcnvintabd  43851  cnvintabd  43854  sqrtcvallem1  43882  reabsifneg  43883  fsovrfovd  44260  ntrclsiso  44318  ntrneifv3  44333  ntrneineine0lem  44334  ntrneicls11  44341  suprleubrd  44417  suprlubrd  44419  lemuldiv4d  44422  pm14.122a  44673  3impexpbicomi  44732  onfrALTlem5  44793  bitr3VD  45099  onfrALTlem5VD  45135  csbrngVD  45146  pwpwuni  45312  supxrre3  45580  xrralrecnnge  45644  eliooshift  45762  limsupre2lem  45978  liminflimsupclim  46061  xlimbr  46081  smfrec  47043  fsetprcnexALT  47318  f1cof1b  47333  reuf1odnf  47363  2reuimp  47371  ralbinrald  47378  afvco2  47432  dfatdmfcoafv2  47510  recnmulnred  47561  sqrtnegnre  47563  subsubelfzo0  47582  ceilbi  47589  ichcircshi  47710  sprvalpwle2  47745  sprsymrelf1lem  47747  sbcpr  47777  poprelb  47780  31prm  47853  requad01  47877  dfeven3  47914  iseven5  47920  0noddALTV  47945  2noddALTV  47949  fpprmod  47983  sbgoldbaltlem1  48035  bgoldbtbndlem2  48062  dfclnbgr2  48079  dfsclnbgr2  48102  dfvopnbgr2  48109  dfsclnbgr6  48114  isuspgrim0lem  48149  usgrgrtrirex  48206  usgrexmpl2nb1  48288  usgrexmpl2nb2  48289  pgnbgreunbgrlem2lem1  48370  pgnbgreunbgrlem2lem2  48371  pgnbgreunbgrlem2lem3  48372  pgn4cyclex  48382  0nodd  48426  2nodd  48428  isassintop  48466  uzlidlring  48491  funcringcsetcALTV2lem8  48553  funcringcsetclem8ALTV  48576  nn0sumltlt  48606  ply1mulgsumlem2  48643  islindeps  48709  lindslinindsimp1  48713  lindslinindsimp2  48719  snlindsntor  48727  zlmodzxznm  48753  ldepslinc  48765  elbigo2  48808  elbigolo1  48813  logblt1b  48820  fldivexpfllog2  48821  nnolog2flm1  48846  digexp  48863  nn0sumshdiglemB  48876  itsclquadeu  49033  itscnhlinecirc02p  49041  ipolublem  49241  ipoglblem  49244