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  2526  euor2  2606  eqabcdv  2862  necon3bbid  2962  necon4bbid  2966  ralanid  3077  rexanid  3078  sbralieALT  3316  ralcom2  3340  rmoanid  3353  reuanid  3354  rabrabi  3414  gencbvex  3496  sbhypfOLD  3500  alexeqg  3606  clel2g  3614  clel3g  3616  clel4g  3618  reurab  3661  reu8  3693  sbceq2a  3754  sbcco2  3769  reu8nf  3829  notabw  4264  2reu4lem  4473  reurexprg  4656  raltpd  4733  ssdifsn  4739  uniprg  4874  disjxun  5090  opabidw  5467  opabid  5468  soeq2  5549  sotrine  5567  posn  5705  xpiindi  5778  dmopab2rex  5860  elpredg  6263  fvopab6  6964  cbvfo  7226  f1eqcocnv  7238  isoid  7266  isoini  7275  isosolem  7284  riotaeqimp  7332  riotarab  7348  resoprab2  7468  tfisi  7792  tfinds2  7797  f1oweALT  7907  dfoprab3  7989  opiota  7994  xpord2indlem  8080  xpord3inddlem  8087  mpocurryd  8202  oalimcl  8478  omword  8488  oeword  8508  nnacan  8546  nnmcan  8552  mapsnd  8813  findcard2s  9079  funisfsupp  9257  suppeqfsuppbi  9269  eqinf  9375  inflb  9380  infglb  9381  infglbb  9382  infltoreq  9394  infempty  9399  brwdomn0  9461  cantnfp1lem3  9576  ssrankr1  9731  r1pw  9741  djulf1o  9808  djurf1o  9809  aleph11  9978  alephval3  10004  gch-kn  10571  wunex2  10632  lttri2  11198  wloglei  11652  divne0b  11790  lemul1  11976  nnnle0  12161  div4p1lem1div2  12379  nn0ind-raph  12576  zindd  12577  suprfinzcl  12590  rebtwnz  12848  qreccl  12870  elpq  12876  xrlttri2  13044  2resupmax  13090  xmulneg1  13171  iooshf  13329  difreicc  13387  fzofzim  13612  elfzomelpfzo  13674  elfznelfzo  13675  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  14565  pfxn0  14593  swrdswrd  14611  pfxccat3  14640  repswswrd  14690  cshf1  14716  cshw1repsw  14729  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  18605  issubm2  18678  mgm2nsgrplem2  18793  nsgacs  19041  cycsubg2  19089  gapm  19185  sscntz  19205  pgrpsubgsymgbi  19287  f1omvdcnv  19323  pmtrprfvalrn  19367  odval2  19430  lsmcntz  19558  rngpropd  20059  rnghmf1o  20337  isrngim2  20338  rhmf1o  20376  isrim  20377  isrimOLD  20378  dfprm2  21380  pzriprnglem10  21397  psgnfix2  21506  islinds3  21741  islindf4  21745  snifpsrbag  21827  gsumply1eq  22194  mdetdiaglem  22483  mdetunilem9  22505  slesolinv  22565  slesolex  22567  cpmatel2  22598  m2cpmghm  22629  m2cpminvid2  22640  pm2mpf1  22684  chfacfscmul0  22743  chfacfscmulfsupp  22744  chfacfpmmul0  22747  chfacfpmmulfsupp  22748  isopn2  22917  cmpsub  23285  connsub  23306  ncvs1  25055  rrxmvallem  25302  itg1mulc  25603  lhop1  25917  mdegleb  25967  lawcos  26724  leibpi  26850  2lgslem1a  27300  2sq2  27342  sletric  27674  bdayon  28178  n0subs2  28259  0reno  28366  colinearalg  28855  edg0iedg0  29000  uhgreq12g  29010  uhgrvtxedgiedgb  29081  usgredg2v  29172  edg0usgr  29198  dfnbgr2  29282  nbuhgr  29288  nbusgredgeu0  29313  nb3grprlem1  29325  nb3grpr  29327  uvtx2vtx1edgb  29344  redwlk  29616  uhgrwkspthlem2  29699  usgr2wlkspth  29704  pthdlem1  29711  cyclnspth  29746  crctcshwlkn0lem1  29755  crctcshwlkn0lem4  29758  crctcsh  29769  iswwlksnx  29785  wwlksm1edg  29826  wwlksnextsurj  29845  wwlksnextproplem3  29856  2wlkdlem4  29873  2wlkdlem5  29874  2pthdlem1  29875  s3wwlks2on  29901  wpthswwlks2on  29906  elwspths2spth  29912  rusgrnumwwlks  29919  umgrclwwlkge2  29935  clwlkclwwlklem2a4  29941  clwlkclwwlk  29946  clwlkclwwlkflem  29948  clwwisshclwws  29959  isclwwlknx  29980  clwwlknwwlksnb  29999  eclclwwlkn1  30019  clwwlknonel  30039  clwwlknun  30056  3wlkdlem6  30109  frgrncvvdeqlem9  30251  fusgreg2wsp  30280  numclwwlk2lem1lem  30286  extwwlkfab  30296  frgrreggt1  30337  ubthlem1  30814  norm-i  31073  hoeq  31704  nmopgt0  31856  pjimai  32120  chirredi  32338  addltmulALT  32390  bian1d  32400  opreu2reuALT  32421  sbcies  32432  rmounid  32439  iunrdx  32507  disjrdx  32535  sgnneg  32778  sgn3da  32779  archiabl  33140  islbs5  33317  ist0cld  33800  oms0  34265  eulerpartgbij  34340  reprinrn  34586  usgrgt2cycl  35107  satfv1lem  35339  satf0op  35354  dmopab3rexdif  35382  satefvfmla0  35395  mrsubrn  35490  topfne  36332  unbdqndv1  36486  bj-hbntbi  36682  bj-issetwt  36853  bj-clel3gALT  37026  copsex2d  37117  bj-elid6  37148  dfgcd3  37302  topdifinfeq  37328  wl-sbalnae  37540  sin2h  37594  poimirlem16  37620  poimirlem17  37621  poimirlem25  37629  mbfresfi  37650  itg2addnclem  37655  itg2addnclem2  37656  itg2addnclem3  37657  ftc1anclem1  37677  isidlc  37999  eldmressnALTV  38251  islshpsm  38963  lshpkrlem1  39093  opcon1b  39181  lautlt  40074  lauteq  40078  idlaut  40079  diblsmopel  41154  doch11  41356  recbothd  41969  aks4d1p8d2  42062  aks4d1p8  42064  isprimroot2  42071  posbezout  42077  aks6d1c5lem1  42113  sticksstones1  42123  sticksstones11  42133  sticksstones22  42145  aks6d1c6lem3  42149  aks6d1c6lem4  42150  aks6d1c7  42161  aks5lem8  42178  f1o2d2  42210  dvdsexpnn0  42311  redvmptabs  42337  prjsprellsp  42588  prjspeclsp  42589  abbibw  42654  istopclsd  42677  eqrabdioph  42754  rexzrexnn0  42781  zindbi  42923  expdiophlem2  42999  onsupeqmax  43223  onsupeqnmax  43224  ordeldif  43235  infordmin  43509  inintabd  43556  cnvcnvintabd  43577  cnvintabd  43580  sqrtcvallem1  43608  reabsifneg  43609  fsovrfovd  43986  ntrclsiso  44044  ntrneifv3  44059  ntrneineine0lem  44060  ntrneicls11  44067  suprleubrd  44143  suprlubrd  44145  lemuldiv4d  44148  pm14.122a  44399  3impexpbicomi  44459  onfrALTlem5  44520  bitr3VD  44826  onfrALTlem5VD  44862  csbrngVD  44873  pwpwuni  45039  supxrre3  45309  xrralrecnnge  45373  eliooshift  45491  limsupre2lem  45709  liminflimsupclim  45792  xlimbr  45812  smfrec  46774  fsetprcnexALT  47050  f1cof1b  47065  reuf1odnf  47095  2reuimp  47103  ralbinrald  47110  afvco2  47164  dfatdmfcoafv2  47242  recnmulnred  47293  sqrtnegnre  47295  subsubelfzo0  47314  ceilbi  47321  ichcircshi  47442  sprvalpwle2  47477  sprsymrelf1lem  47479  sbcpr  47509  poprelb  47512  31prm  47585  requad01  47609  dfeven3  47646  iseven5  47652  0noddALTV  47677  2noddALTV  47681  fpprmod  47715  sbgoldbaltlem1  47767  bgoldbtbndlem2  47794  dfclnbgr2  47811  dfsclnbgr2  47834  dfvopnbgr2  47841  dfsclnbgr6  47846  isuspgrim0lem  47881  usgrgrtrirex  47938  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgn4cyclex  48114  0nodd  48158  2nodd  48160  isassintop  48198  uzlidlring  48223  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  nn0sumltlt  48338  ply1mulgsumlem2  48376  islindeps  48442  lindslinindsimp1  48446  lindslinindsimp2  48452  snlindsntor  48460  zlmodzxznm  48486  ldepslinc  48498  elbigo2  48541  elbigolo1  48546  logblt1b  48553  fldivexpfllog2  48554  nnolog2flm1  48579  digexp  48596  nn0sumshdiglemB  48609  itsclquadeu  48766  itscnhlinecirc02p  48774  ipolublem  48974  ipoglblem  48977