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  4260  2reu4lem  4469  reurexprg  4654  raltpd  4731  ssdifsn  4737  uniprg  4872  disjxun  5087  opabidw  5462  opabid  5463  soeq2  5544  sotrine  5562  posn  5700  xpiindi  5774  dmopab2rex  5856  elpredg  6262  fvopab6  6963  cbvfo  7223  f1eqcocnv  7235  isoid  7263  isoini  7272  isosolem  7281  riotaeqimp  7329  riotarab  7345  resoprab2  7465  tfisi  7789  tfinds2  7794  f1oweALT  7904  dfoprab3  7986  opiota  7991  xpord2indlem  8077  xpord3inddlem  8084  mpocurryd  8199  oalimcl  8475  omword  8485  oeword  8505  nnacan  8543  nnmcan  8549  mapsnd  8810  findcard2s  9075  funisfsupp  9251  suppeqfsuppbi  9263  eqinf  9369  inflb  9374  infglb  9375  infglbb  9376  infltoreq  9388  infempty  9393  brwdomn0  9455  cantnfp1lem3  9570  ssrankr1  9728  r1pw  9738  djulf1o  9805  djurf1o  9806  aleph11  9975  alephval3  10001  gch-kn  10568  wunex2  10629  lttri2  11195  wloglei  11649  divne0b  11787  lemul1  11973  nnnle0  12158  div4p1lem1div2  12376  nn0ind-raph  12573  zindd  12574  suprfinzcl  12587  rebtwnz  12845  qreccl  12867  elpq  12873  xrlttri2  13041  2resupmax  13087  xmulneg1  13168  iooshf  13326  difreicc  13384  fzofzim  13609  elfzomelpfzo  13672  elfznelfzo  13673  zmodid2  13803  2submod  13839  modfzo0difsn  13850  om2uzlti  13857  expcan  14076  hashvnfin  14267  hashneq0  14271  prhash2ex  14306  hashgt0elex  14308  hashgt12el  14329  hashgt12el2  14330  hashbclem  14359  hashf1lem2  14363  prprrab  14380  swrd0  14566  pfxn0  14594  swrdswrd  14612  pfxccat3  14641  repswswrd  14691  cshf1  14717  cshw1repsw  14730  relexpindlem  14970  absz  15218  iserex  15564  prodrb  15839  absdvdsb  16185  dvdsabsb  16186  modmulconst  16199  dvdsadd  16213  dvdsabseq  16224  mod2eq0even  16257  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  zeo5  16267  sadadd2lem2  16361  smupvallem  16394  gcdass  16458  lcmdvds  16519  lcmass  16525  divgcdcoprm0  16576  divgcdcoprmex  16577  1nprm  16590  dvdsnprmd  16601  prmdvdssq  16629  ncoprmlnprm  16639  isevengcd2  16641  m1dvdsndvds  16710  cshws0  17013  sbcie3s  17073  dfiso2  17679  initoid  17908  termoid  17909  funcestrcsetclem8  18053  lublecllem  18264  odudlatb  18431  sgrppropd  18639  issubm2  18712  mgm2nsgrplem2  18827  nsgacs  19074  cycsubg2  19122  gapm  19218  sscntz  19238  pgrpsubgsymgbi  19320  f1omvdcnv  19356  pmtrprfvalrn  19400  odval2  19463  lsmcntz  19591  rngpropd  20092  rnghmf1o  20370  isrngim2  20371  rhmf1o  20408  isrim  20409  dfprm2  21410  pzriprnglem10  21427  psgnfix2  21536  islinds3  21771  islindf4  21775  snifpsrbag  21857  gsumply1eq  22224  mdetdiaglem  22513  mdetunilem9  22535  slesolinv  22595  slesolex  22597  cpmatel2  22628  m2cpmghm  22659  m2cpminvid2  22670  pm2mpf1  22714  chfacfscmul0  22773  chfacfscmulfsupp  22774  chfacfpmmul0  22777  chfacfpmmulfsupp  22778  isopn2  22947  cmpsub  23315  connsub  23336  ncvs1  25084  rrxmvallem  25331  itg1mulc  25632  lhop1  25946  mdegleb  25996  lawcos  26753  leibpi  26879  2lgslem1a  27329  2sq2  27371  sletric  27703  bdayon  28209  n0subs2  28290  0reno  28399  colinearalg  28888  edg0iedg0  29033  uhgreq12g  29043  uhgrvtxedgiedgb  29114  usgredg2v  29205  edg0usgr  29231  dfnbgr2  29315  nbuhgr  29321  nbusgredgeu0  29346  nb3grprlem1  29358  nb3grpr  29360  uvtx2vtx1edgb  29377  redwlk  29649  uhgrwkspthlem2  29732  usgr2wlkspth  29737  pthdlem1  29744  cyclnspth  29779  crctcshwlkn0lem1  29788  crctcshwlkn0lem4  29791  crctcsh  29802  iswwlksnx  29818  wwlksm1edg  29859  wwlksnextsurj  29878  wwlksnextproplem3  29889  2wlkdlem4  29906  2wlkdlem5  29907  2pthdlem1  29908  s3wwlks2on  29934  sps3wwlks2on  29935  wpthswwlks2on  29942  elwspths2spth  29948  rusgrnumwwlks  29955  umgrclwwlkge2  29971  clwlkclwwlklem2a4  29977  clwlkclwwlk  29982  clwlkclwwlkflem  29984  clwwisshclwws  29995  isclwwlknx  30016  clwwlknwwlksnb  30035  eclclwwlkn1  30055  clwwlknonel  30075  clwwlknun  30092  3wlkdlem6  30145  frgrncvvdeqlem9  30287  fusgreg2wsp  30316  numclwwlk2lem1lem  30322  extwwlkfab  30332  frgrreggt1  30373  ubthlem1  30850  norm-i  31109  hoeq  31740  nmopgt0  31892  pjimai  32156  chirredi  32374  addltmulALT  32426  bian1d  32435  opreu2reuALT  32456  sbcies  32467  rmounid  32474  iunrdx  32543  disjrdx  32571  sgnneg  32816  sgn3da  32817  archiabl  33167  islbs5  33345  ist0cld  33846  oms0  34310  eulerpartgbij  34385  reprinrn  34631  usgrgt2cycl  35174  satfv1lem  35406  satf0op  35421  dmopab3rexdif  35449  satefvfmla0  35462  mrsubrn  35557  topfne  36398  unbdqndv1  36552  bj-hbntbi  36748  bj-issetwt  36919  bj-clel3gALT  37092  copsex2d  37183  bj-elid6  37214  dfgcd3  37368  topdifinfeq  37394  wl-sbalnae  37606  sin2h  37660  poimirlem16  37686  poimirlem17  37687  poimirlem25  37695  mbfresfi  37716  itg2addnclem  37721  itg2addnclem2  37722  itg2addnclem3  37723  ftc1anclem1  37743  isidlc  38065  eldmressnALTV  38321  islshpsm  39089  lshpkrlem1  39219  opcon1b  39307  lautlt  40200  lauteq  40204  idlaut  40205  diblsmopel  41280  doch11  41482  recbothd  42095  aks4d1p8d2  42188  aks4d1p8  42190  isprimroot2  42197  posbezout  42203  aks6d1c5lem1  42239  sticksstones1  42249  sticksstones11  42259  sticksstones22  42271  aks6d1c6lem3  42275  aks6d1c6lem4  42276  aks6d1c7  42287  aks5lem8  42304  f1o2d2  42336  dvdsexpnn0  42437  redvmptabs  42463  prjsprellsp  42714  prjspeclsp  42715  abbibw  42780  istopclsd  42803  eqrabdioph  42880  rexzrexnn0  42907  zindbi  43049  expdiophlem2  43125  onsupeqmax  43349  onsupeqnmax  43350  ordeldif  43361  infordmin  43635  inintabd  43682  cnvcnvintabd  43703  cnvintabd  43706  sqrtcvallem1  43734  reabsifneg  43735  fsovrfovd  44112  ntrclsiso  44170  ntrneifv3  44185  ntrneineine0lem  44186  ntrneicls11  44193  suprleubrd  44269  suprlubrd  44271  lemuldiv4d  44274  pm14.122a  44525  3impexpbicomi  44584  onfrALTlem5  44645  bitr3VD  44951  onfrALTlem5VD  44987  csbrngVD  44998  pwpwuni  45164  supxrre3  45434  xrralrecnnge  45498  eliooshift  45616  limsupre2lem  45832  liminflimsupclim  45915  xlimbr  45935  smfrec  46897  fsetprcnexALT  47172  f1cof1b  47187  reuf1odnf  47217  2reuimp  47225  ralbinrald  47232  afvco2  47286  dfatdmfcoafv2  47364  recnmulnred  47415  sqrtnegnre  47417  subsubelfzo0  47436  ceilbi  47443  ichcircshi  47564  sprvalpwle2  47599  sprsymrelf1lem  47601  sbcpr  47631  poprelb  47634  31prm  47707  requad01  47731  dfeven3  47768  iseven5  47774  0noddALTV  47799  2noddALTV  47803  fpprmod  47837  sbgoldbaltlem1  47889  bgoldbtbndlem2  47916  dfclnbgr2  47933  dfsclnbgr2  47956  dfvopnbgr2  47963  dfsclnbgr6  47968  isuspgrim0lem  48003  usgrgrtrirex  48060  usgrexmpl2nb1  48142  usgrexmpl2nb2  48143  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgnbgreunbgrlem2lem3  48226  pgn4cyclex  48236  0nodd  48280  2nodd  48282  isassintop  48320  uzlidlring  48345  funcringcsetcALTV2lem8  48407  funcringcsetclem8ALTV  48430  nn0sumltlt  48460  ply1mulgsumlem2  48498  islindeps  48564  lindslinindsimp1  48568  lindslinindsimp2  48574  snlindsntor  48582  zlmodzxznm  48608  ldepslinc  48620  elbigo2  48663  elbigolo1  48668  logblt1b  48675  fldivexpfllog2  48676  nnolog2flm1  48701  digexp  48718  nn0sumshdiglemB  48731  itsclquadeu  48888  itscnhlinecirc02p  48896  ipolublem  49096  ipoglblem  49099