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  3324  ralcom2  3348  rmoanid  3361  reuanid  3362  rabrabi  3422  gencbvex  3504  sbhypfOLD  3508  alexeqg  3614  clel2g  3622  clel3g  3624  clel4g  3626  reurab  3669  reu8  3701  sbceq2a  3762  sbcco2  3777  reu8nf  3837  notabw  4272  2reu4lem  4481  reurexprg  4664  raltpd  4741  ssdifsn  4748  uniprg  4883  disjxun  5100  opabidw  5479  opabid  5480  soeq2  5561  sotrine  5579  posn  5717  xpiindi  5789  dmopab2rex  5871  elpredg  6276  fvopab6  6984  cbvfo  7246  f1eqcocnv  7258  isoid  7286  isoini  7295  isosolem  7304  riotaeqimp  7352  riotarab  7368  resoprab2  7488  tfisi  7815  tfinds2  7820  f1oweALT  7930  dfoprab3  8012  opiota  8017  xpord2indlem  8103  xpord3inddlem  8110  mpocurryd  8225  oalimcl  8501  omword  8511  oeword  8531  nnacan  8569  nnmcan  8575  mapsnd  8836  findcard2s  9106  funisfsupp  9294  suppeqfsuppbi  9306  eqinf  9412  inflb  9417  infglb  9418  infglbb  9419  infltoreq  9431  infempty  9436  brwdomn0  9498  cantnfp1lem3  9609  ssrankr1  9764  r1pw  9774  djulf1o  9841  djurf1o  9842  aleph11  10013  alephval3  10039  gch-kn  10606  wunex2  10667  lttri2  11232  wloglei  11686  divne0b  11824  lemul1  12010  nnnle0  12195  div4p1lem1div2  12413  nn0ind-raph  12610  zindd  12611  suprfinzcl  12624  rebtwnz  12882  qreccl  12904  elpq  12910  xrlttri2  13078  2resupmax  13124  xmulneg1  13205  iooshf  13363  difreicc  13421  fzofzim  13646  elfzomelpfzo  13708  elfznelfzo  13709  zmodid2  13837  2submod  13873  modfzo0difsn  13884  om2uzlti  13891  expcan  14110  hashvnfin  14301  hashneq0  14305  prhash2ex  14340  hashgt0elex  14342  hashgt12el  14363  hashgt12el2  14364  hashbclem  14393  hashf1lem2  14397  prprrab  14414  swrd0  14599  pfxn0  14627  swrdswrd  14646  pfxccat3  14675  repswswrd  14725  cshf1  14751  cshw1repsw  14764  relexpindlem  15005  absz  15253  iserex  15599  prodrb  15874  absdvdsb  16220  dvdsabsb  16221  modmulconst  16234  dvdsadd  16248  dvdsabseq  16259  mod2eq0even  16292  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  zeo5  16302  sadadd2lem2  16396  smupvallem  16429  gcdass  16493  lcmdvds  16554  lcmass  16560  divgcdcoprm0  16611  divgcdcoprmex  16612  1nprm  16625  dvdsnprmd  16636  prmdvdssq  16664  ncoprmlnprm  16674  isevengcd2  16676  m1dvdsndvds  16745  cshws0  17048  sbcie3s  17108  dfiso2  17714  initoid  17943  termoid  17944  funcestrcsetclem8  18088  lublecllem  18299  odudlatb  18466  sgrppropd  18640  issubm2  18713  mgm2nsgrplem2  18828  nsgacs  19076  cycsubg2  19124  gapm  19220  sscntz  19240  pgrpsubgsymgbi  19322  f1omvdcnv  19358  pmtrprfvalrn  19402  odval2  19465  lsmcntz  19593  rngpropd  20094  rnghmf1o  20372  isrngim2  20373  rhmf1o  20411  isrim  20412  isrimOLD  20413  dfprm2  21415  pzriprnglem10  21432  psgnfix2  21541  islinds3  21776  islindf4  21780  snifpsrbag  21862  gsumply1eq  22229  mdetdiaglem  22518  mdetunilem9  22540  slesolinv  22600  slesolex  22602  cpmatel2  22633  m2cpmghm  22664  m2cpminvid2  22675  pm2mpf1  22719  chfacfscmul0  22778  chfacfscmulfsupp  22779  chfacfpmmul0  22782  chfacfpmmulfsupp  22783  isopn2  22952  cmpsub  23320  connsub  23341  ncvs1  25090  rrxmvallem  25337  itg1mulc  25638  lhop1  25952  mdegleb  26002  lawcos  26759  leibpi  26885  2lgslem1a  27335  2sq2  27377  sletric  27709  bdayon  28213  n0subs2  28294  0reno  28401  colinearalg  28890  edg0iedg0  29035  uhgreq12g  29045  uhgrvtxedgiedgb  29116  usgredg2v  29207  edg0usgr  29233  dfnbgr2  29317  nbuhgr  29323  nbusgredgeu0  29348  nb3grprlem1  29360  nb3grpr  29362  uvtx2vtx1edgb  29379  redwlk  29651  uhgrwkspthlem2  29734  usgr2wlkspth  29739  pthdlem1  29746  cyclnspth  29781  crctcshwlkn0lem1  29790  crctcshwlkn0lem4  29793  crctcsh  29804  iswwlksnx  29820  wwlksm1edg  29861  wwlksnextsurj  29880  wwlksnextproplem3  29891  2wlkdlem4  29908  2wlkdlem5  29909  2pthdlem1  29910  s3wwlks2on  29936  wpthswwlks2on  29941  elwspths2spth  29947  rusgrnumwwlks  29954  umgrclwwlkge2  29970  clwlkclwwlklem2a4  29976  clwlkclwwlk  29981  clwlkclwwlkflem  29983  clwwisshclwws  29994  isclwwlknx  30015  clwwlknwwlksnb  30034  eclclwwlkn1  30054  clwwlknonel  30074  clwwlknun  30091  3wlkdlem6  30144  frgrncvvdeqlem9  30286  fusgreg2wsp  30315  numclwwlk2lem1lem  30321  extwwlkfab  30331  frgrreggt1  30372  ubthlem1  30849  norm-i  31108  hoeq  31739  nmopgt0  31891  pjimai  32155  chirredi  32373  addltmulALT  32425  bian1d  32435  opreu2reuALT  32456  sbcies  32467  rmounid  32474  iunrdx  32542  disjrdx  32570  sgnneg  32808  sgn3da  32809  archiabl  33167  islbs5  33344  ist0cld  33816  oms0  34281  eulerpartgbij  34356  reprinrn  34602  usgrgt2cycl  35110  satfv1lem  35342  satf0op  35357  dmopab3rexdif  35385  satefvfmla0  35398  mrsubrn  35493  topfne  36335  unbdqndv1  36489  bj-hbntbi  36685  bj-issetwt  36856  bj-clel3gALT  37029  copsex2d  37120  bj-elid6  37151  dfgcd3  37305  topdifinfeq  37331  wl-sbalnae  37543  sin2h  37597  poimirlem16  37623  poimirlem17  37624  poimirlem25  37632  mbfresfi  37653  itg2addnclem  37658  itg2addnclem2  37659  itg2addnclem3  37660  ftc1anclem1  37680  isidlc  38002  eldmressnALTV  38254  islshpsm  38966  lshpkrlem1  39096  opcon1b  39184  lautlt  40078  lauteq  40082  idlaut  40083  diblsmopel  41158  doch11  41360  recbothd  41973  aks4d1p8d2  42066  aks4d1p8  42068  isprimroot2  42075  posbezout  42081  aks6d1c5lem1  42117  sticksstones1  42127  sticksstones11  42137  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c7  42165  aks5lem8  42182  f1o2d2  42214  dvdsexpnn0  42315  redvmptabs  42341  prjsprellsp  42592  prjspeclsp  42593  abbibw  42658  istopclsd  42681  eqrabdioph  42758  rexzrexnn0  42785  zindbi  42928  expdiophlem2  43004  onsupeqmax  43228  onsupeqnmax  43229  ordeldif  43240  infordmin  43514  inintabd  43561  cnvcnvintabd  43582  cnvintabd  43585  sqrtcvallem1  43613  reabsifneg  43614  fsovrfovd  43991  ntrclsiso  44049  ntrneifv3  44064  ntrneineine0lem  44065  ntrneicls11  44072  suprleubrd  44148  suprlubrd  44150  lemuldiv4d  44153  pm14.122a  44404  3impexpbicomi  44464  onfrALTlem5  44525  bitr3VD  44831  onfrALTlem5VD  44867  csbrngVD  44878  pwpwuni  45044  supxrre3  45314  xrralrecnnge  45379  eliooshift  45497  limsupre2lem  45715  liminflimsupclim  45798  xlimbr  45818  smfrec  46780  fsetprcnexALT  47056  f1cof1b  47071  reuf1odnf  47101  2reuimp  47109  ralbinrald  47116  afvco2  47170  dfatdmfcoafv2  47248  recnmulnred  47299  sqrtnegnre  47301  subsubelfzo0  47320  ceilbi  47327  ichcircshi  47448  sprvalpwle2  47483  sprsymrelf1lem  47485  sbcpr  47515  poprelb  47518  31prm  47591  requad01  47615  dfeven3  47652  iseven5  47658  0noddALTV  47683  2noddALTV  47687  fpprmod  47721  sbgoldbaltlem1  47773  bgoldbtbndlem2  47800  dfclnbgr2  47817  dfsclnbgr2  47839  dfvopnbgr2  47846  dfsclnbgr6  47851  isuspgrim0lem  47886  usgrgrtrirex  47942  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgn4cyclex  48109  0nodd  48151  2nodd  48153  isassintop  48191  uzlidlring  48216  funcringcsetcALTV2lem8  48278  funcringcsetclem8ALTV  48301  nn0sumltlt  48331  ply1mulgsumlem2  48369  islindeps  48435  lindslinindsimp1  48439  lindslinindsimp2  48445  snlindsntor  48453  zlmodzxznm  48479  ldepslinc  48491  elbigo2  48534  elbigolo1  48539  logblt1b  48546  fldivexpfllog2  48547  nnolog2flm1  48572  digexp  48589  nn0sumshdiglemB  48602  itsclquadeu  48759  itscnhlinecirc02p  48767  ipolublem  48967  ipoglblem  48970