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  2255  sbal1  2528  euor2  2608  eqabcdv  2865  necon3bbid  2965  necon4bbid  2969  ralanid  3080  rexanid  3081  sbralieALT  3319  ralcom2  3343  rmoanid  3356  reuanid  3357  rabrabi  3414  gencbvex  3495  alexeqg  3601  clel2g  3609  clel3g  3611  clel4g  3613  reurab  3655  reu8  3687  sbceq2a  3748  sbcco2  3763  reu8nf  3823  notabw  4262  2reu4lem  4471  reurexprg  4656  raltpd  4733  ssdifsn  4739  uniprg  4874  disjxun  5091  opabidw  5467  opabid  5468  soeq2  5549  sotrine  5567  posn  5705  xpiindi  5780  dmopab2rex  5862  elpredg  6268  fvopab6  6969  cbvfo  7229  f1eqcocnv  7241  isoid  7269  isoini  7278  isosolem  7287  riotaeqimp  7335  riotarab  7351  resoprab2  7471  tfisi  7795  tfinds2  7800  f1oweALT  7910  dfoprab3  7992  opiota  7997  xpord2indlem  8083  xpord3inddlem  8090  mpocurryd  8205  oalimcl  8481  omword  8491  oeword  8511  nnacan  8549  nnmcan  8555  mapsnd  8816  findcard2s  9081  funisfsupp  9257  suppeqfsuppbi  9269  eqinf  9375  inflb  9380  infglb  9381  infglbb  9382  infltoreq  9394  infempty  9399  brwdomn0  9461  cantnfp1lem3  9576  ssrankr1  9734  r1pw  9744  djulf1o  9811  djurf1o  9812  aleph11  9981  alephval3  10007  gch-kn  10574  wunex2  10635  lttri2  11201  wloglei  11655  divne0b  11793  lemul1  11979  nnnle0  12164  div4p1lem1div2  12382  nn0ind-raph  12579  zindd  12580  suprfinzcl  12593  rebtwnz  12851  qreccl  12873  elpq  12879  xrlttri2  13047  2resupmax  13093  xmulneg1  13174  iooshf  13332  difreicc  13390  fzofzim  13615  elfzomelpfzo  13678  elfznelfzo  13679  zmodid2  13809  2submod  13845  modfzo0difsn  13856  om2uzlti  13863  expcan  14082  hashvnfin  14273  hashneq0  14277  prhash2ex  14312  hashgt0elex  14314  hashgt12el  14335  hashgt12el2  14336  hashbclem  14365  hashf1lem2  14369  prprrab  14386  swrd0  14572  pfxn0  14600  swrdswrd  14618  pfxccat3  14647  repswswrd  14697  cshf1  14723  cshw1repsw  14736  relexpindlem  14976  absz  15224  iserex  15570  prodrb  15845  absdvdsb  16191  dvdsabsb  16192  modmulconst  16205  dvdsadd  16219  dvdsabseq  16230  mod2eq0even  16263  oddnn02np1  16265  oddge22np1  16266  evennn02n  16267  evennn2n  16268  zeo5  16273  sadadd2lem2  16367  smupvallem  16400  gcdass  16464  lcmdvds  16525  lcmass  16531  divgcdcoprm0  16582  divgcdcoprmex  16583  1nprm  16596  dvdsnprmd  16607  prmdvdssq  16635  ncoprmlnprm  16645  isevengcd2  16647  m1dvdsndvds  16716  cshws0  17019  sbcie3s  17079  dfiso2  17685  initoid  17914  termoid  17915  funcestrcsetclem8  18059  lublecllem  18270  odudlatb  18437  sgrppropd  18645  issubm2  18718  mgm2nsgrplem2  18833  nsgacs  19080  cycsubg2  19128  gapm  19224  sscntz  19244  pgrpsubgsymgbi  19326  f1omvdcnv  19362  pmtrprfvalrn  19406  odval2  19469  lsmcntz  19597  rngpropd  20098  rnghmf1o  20376  isrngim2  20377  rhmf1o  20414  isrim  20415  dfprm2  21416  pzriprnglem10  21433  psgnfix2  21542  islinds3  21777  islindf4  21781  snifpsrbag  21863  gsumply1eq  22230  mdetdiaglem  22519  mdetunilem9  22541  slesolinv  22601  slesolex  22603  cpmatel2  22634  m2cpmghm  22665  m2cpminvid2  22676  pm2mpf1  22720  chfacfscmul0  22779  chfacfscmulfsupp  22780  chfacfpmmul0  22783  chfacfpmmulfsupp  22784  isopn2  22953  cmpsub  23321  connsub  23342  ncvs1  25090  rrxmvallem  25337  itg1mulc  25638  lhop1  25952  mdegleb  26002  lawcos  26759  leibpi  26885  2lgslem1a  27335  2sq2  27377  sletric  27709  bdayon  28215  n0subs2  28296  0reno  28405  colinearalg  28895  edg0iedg0  29040  uhgreq12g  29050  uhgrvtxedgiedgb  29121  usgredg2v  29212  edg0usgr  29238  dfnbgr2  29322  nbuhgr  29328  nbusgredgeu0  29353  nb3grprlem1  29365  nb3grpr  29367  uvtx2vtx1edgb  29384  redwlk  29656  uhgrwkspthlem2  29739  usgr2wlkspth  29744  pthdlem1  29751  cyclnspth  29786  crctcshwlkn0lem1  29795  crctcshwlkn0lem4  29798  crctcsh  29809  iswwlksnx  29825  wwlksm1edg  29866  wwlksnextsurj  29885  wwlksnextproplem3  29896  2wlkdlem4  29913  2wlkdlem5  29914  2pthdlem1  29915  s3wwlks2on  29941  sps3wwlks2on  29942  wpthswwlks2on  29949  elwspths2spth  29955  rusgrnumwwlks  29962  umgrclwwlkge2  29978  clwlkclwwlklem2a4  29984  clwlkclwwlk  29989  clwlkclwwlkflem  29991  clwwisshclwws  30002  isclwwlknx  30023  clwwlknwwlksnb  30042  eclclwwlkn1  30062  clwwlknonel  30082  clwwlknun  30099  3wlkdlem6  30152  frgrncvvdeqlem9  30294  fusgreg2wsp  30323  numclwwlk2lem1lem  30329  extwwlkfab  30339  frgrreggt1  30380  ubthlem1  30857  norm-i  31116  hoeq  31747  nmopgt0  31899  pjimai  32163  chirredi  32381  addltmulALT  32433  bian1d  32442  opreu2reuALT  32463  sbcies  32474  rmounid  32481  iunrdx  32550  disjrdx  32578  sgnneg  32823  sgn3da  32824  archiabl  33174  islbs5  33352  ist0cld  33853  oms0  34317  eulerpartgbij  34392  reprinrn  34638  usgrgt2cycl  35181  satfv1lem  35413  satf0op  35428  dmopab3rexdif  35456  satefvfmla0  35469  mrsubrn  35564  topfne  36405  unbdqndv1  36559  bj-hbntbi  36755  bj-issetwt  36926  bj-clel3gALT  37099  copsex2d  37190  bj-elid6  37221  dfgcd3  37375  topdifinfeq  37401  wl-sbalnae  37613  sin2h  37656  poimirlem16  37682  poimirlem17  37683  poimirlem25  37691  mbfresfi  37712  itg2addnclem  37717  itg2addnclem2  37718  itg2addnclem3  37719  ftc1anclem1  37739  isidlc  38061  eldmressnALTV  38317  islshpsm  39085  lshpkrlem1  39215  opcon1b  39303  lautlt  40196  lauteq  40200  idlaut  40201  diblsmopel  41276  doch11  41478  recbothd  42091  aks4d1p8d2  42184  aks4d1p8  42186  isprimroot2  42193  posbezout  42199  aks6d1c5lem1  42235  sticksstones1  42245  sticksstones11  42255  sticksstones22  42267  aks6d1c6lem3  42271  aks6d1c6lem4  42272  aks6d1c7  42283  aks5lem8  42300  f1o2d2  42332  dvdsexpnn0  42433  redvmptabs  42459  prjsprellsp  42710  prjspeclsp  42711  abbibw  42776  istopclsd  42798  eqrabdioph  42875  rexzrexnn0  42902  zindbi  43044  expdiophlem2  43120  onsupeqmax  43344  onsupeqnmax  43345  ordeldif  43356  infordmin  43630  inintabd  43677  cnvcnvintabd  43698  cnvintabd  43701  sqrtcvallem1  43729  reabsifneg  43730  fsovrfovd  44107  ntrclsiso  44165  ntrneifv3  44180  ntrneineine0lem  44181  ntrneicls11  44188  suprleubrd  44264  suprlubrd  44266  lemuldiv4d  44269  pm14.122a  44520  3impexpbicomi  44579  onfrALTlem5  44640  bitr3VD  44946  onfrALTlem5VD  44982  csbrngVD  44993  pwpwuni  45159  supxrre3  45429  xrralrecnnge  45493  eliooshift  45611  limsupre2lem  45827  liminflimsupclim  45910  xlimbr  45930  smfrec  46892  fsetprcnexALT  47167  f1cof1b  47182  reuf1odnf  47212  2reuimp  47220  ralbinrald  47227  afvco2  47281  dfatdmfcoafv2  47359  recnmulnred  47410  sqrtnegnre  47412  subsubelfzo0  47431  ceilbi  47438  ichcircshi  47559  sprvalpwle2  47594  sprsymrelf1lem  47596  sbcpr  47626  poprelb  47629  31prm  47702  requad01  47726  dfeven3  47763  iseven5  47769  0noddALTV  47794  2noddALTV  47798  fpprmod  47832  sbgoldbaltlem1  47884  bgoldbtbndlem2  47911  dfclnbgr2  47928  dfsclnbgr2  47951  dfvopnbgr2  47958  dfsclnbgr6  47963  isuspgrim0lem  47998  usgrgrtrirex  48055  usgrexmpl2nb1  48137  usgrexmpl2nb2  48138  pgnbgreunbgrlem2lem1  48219  pgnbgreunbgrlem2lem2  48220  pgnbgreunbgrlem2lem3  48221  pgn4cyclex  48231  0nodd  48275  2nodd  48277  isassintop  48315  uzlidlring  48340  funcringcsetcALTV2lem8  48402  funcringcsetclem8ALTV  48425  nn0sumltlt  48455  ply1mulgsumlem2  48493  islindeps  48559  lindslinindsimp1  48563  lindslinindsimp2  48569  snlindsntor  48577  zlmodzxznm  48603  ldepslinc  48615  elbigo2  48658  elbigolo1  48663  logblt1b  48670  fldivexpfllog2  48671  nnolog2flm1  48696  digexp  48713  nn0sumshdiglemB  48726  itsclquadeu  48883  itscnhlinecirc02p  48891  ipolublem  49091  ipoglblem  49094