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  835  pm5.55  950  pm5.54  1019  ninba  1023  pm5.75  1030  sbequ12r  2249  sbal1  2530  euor2  2610  eqabcdv  2873  necon3bbid  2975  necon4bbid  2979  ralanid  3092  rexanid  3093  sbralieALT  3356  ralcom2  3374  rmoanid  3387  reuanid  3388  rabrabi  3452  gencbvex  3540  sbhypfOLD  3544  alexeqg  3650  clel2g  3658  clel3g  3660  clel4g  3662  reurab  3709  reu8  3741  sbceq2a  3802  sbcco2  3817  reu8nf  3885  notabw  4318  2reu4lem  4527  reurexprg  4708  raltpd  4785  ssdifsn  4792  uniprg  4927  disjxun  5145  opabidw  5533  opabid  5534  soeq2  5618  sotrine  5635  posn  5773  xpiindi  5848  dmopab2rex  5930  elpredg  6336  fvopab6  7049  cbvfo  7308  f1eqcocnv  7320  isoid  7348  isoini  7357  isosolem  7366  riotaeqimp  7413  riotarab  7429  resoprab2  7551  tfisi  7879  tfinds2  7884  f1oweALT  7995  dfoprab3  8077  opiota  8082  xpord2indlem  8170  xpord3inddlem  8177  mpocurryd  8292  oalimcl  8596  omword  8606  oeword  8626  nnacan  8664  nnmcan  8670  mapsnd  8924  findcard2s  9203  funisfsupp  9404  suppeqfsuppbi  9416  eqinf  9521  inflb  9526  infglb  9527  infglbb  9528  infltoreq  9539  infempty  9544  brwdomn0  9606  cantnfp1lem3  9717  ssrankr1  9872  r1pw  9882  djulf1o  9949  djurf1o  9950  aleph11  10121  alephval3  10147  gch-kn  10714  wunex2  10775  lttri2  11340  wloglei  11792  divne0b  11930  lemul1  12116  nnnle0  12296  div4p1lem1div2  12518  nn0ind-raph  12715  zindd  12716  suprfinzcl  12729  rebtwnz  12986  qreccl  13008  elpq  13014  xrlttri2  13180  2resupmax  13226  xmulneg1  13307  iooshf  13462  difreicc  13520  fzofzim  13745  elfzomelpfzo  13806  elfznelfzo  13807  zmodid2  13935  2submod  13969  modfzo0difsn  13980  om2uzlti  13987  expcan  14205  hashvnfin  14395  hashneq0  14399  prhash2ex  14434  hashgt0elex  14436  hashgt12el  14457  hashgt12el2  14458  hashbclem  14487  hashf1lem2  14491  prprrab  14508  swrd0  14692  pfxn0  14720  swrdswrd  14739  pfxccat3  14768  repswswrd  14818  cshf1  14844  cshw1repsw  14857  relexpindlem  15098  absz  15346  iserex  15689  prodrb  15964  absdvdsb  16308  dvdsabsb  16309  modmulconst  16321  dvdsadd  16335  dvdsabseq  16346  mod2eq0even  16379  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  zeo5  16389  sadadd2lem2  16483  smupvallem  16516  gcdass  16580  lcmdvds  16641  lcmass  16647  divgcdcoprm0  16698  divgcdcoprmex  16699  1nprm  16712  dvdsnprmd  16723  prmdvdssq  16751  ncoprmlnprm  16761  isevengcd2  16763  m1dvdsndvds  16831  cshws0  17135  sbcie3s  17195  dfiso2  17819  initoid  18054  termoid  18055  funcestrcsetclem8  18202  lublecllem  18417  odudlatb  18582  sgrppropd  18756  issubm2  18829  mgm2nsgrplem2  18944  nsgacs  19192  cycsubg2  19240  gapm  19336  sscntz  19356  pgrpsubgsymgbi  19440  f1omvdcnv  19476  pmtrprfvalrn  19520  odval2  19583  lsmcntz  19711  rngpropd  20191  rnghmf1o  20468  isrngim2  20469  rhmf1o  20507  isrim  20508  isrimOLD  20509  dfprm2  21501  pzriprnglem10  21518  psgnfix2  21634  islinds3  21871  islindf4  21875  snifpsrbag  21957  gsumply1eq  22328  mdetdiaglem  22619  mdetunilem9  22641  slesolinv  22701  slesolex  22703  cpmatel2  22734  m2cpmghm  22765  m2cpminvid2  22776  pm2mpf1  22820  chfacfscmul0  22879  chfacfscmulfsupp  22880  chfacfpmmul0  22883  chfacfpmmulfsupp  22884  isopn2  23055  cmpsub  23423  connsub  23444  ncvs1  25204  rrxmvallem  25451  itg1mulc  25753  lhop1  26067  mdegleb  26117  lawcos  26873  leibpi  26999  2lgslem1a  27449  2sq2  27491  sletric  27823  0reno  28443  colinearalg  28939  edg0iedg0  29086  uhgreq12g  29096  uhgrvtxedgiedgb  29167  usgredg2v  29258  edg0usgr  29284  dfnbgr2  29368  nbuhgr  29374  nbusgredgeu0  29399  nb3grprlem1  29411  nb3grpr  29413  uvtx2vtx1edgb  29430  redwlk  29704  uhgrwkspthlem2  29786  usgr2wlkspth  29791  pthdlem1  29798  cyclnspth  29832  crctcshwlkn0lem1  29839  crctcshwlkn0lem4  29842  crctcsh  29853  iswwlksnx  29869  wwlksm1edg  29910  wwlksnextsurj  29929  wwlksnextproplem3  29940  2wlkdlem4  29957  2wlkdlem5  29958  2pthdlem1  29959  s3wwlks2on  29985  wpthswwlks2on  29990  elwspths2spth  29996  rusgrnumwwlks  30003  umgrclwwlkge2  30019  clwlkclwwlklem2a4  30025  clwlkclwwlk  30030  clwlkclwwlkflem  30032  clwwisshclwws  30043  isclwwlknx  30064  clwwlknwwlksnb  30083  eclclwwlkn1  30103  clwwlknonel  30123  clwwlknun  30140  3wlkdlem6  30193  frgrncvvdeqlem9  30335  fusgreg2wsp  30364  numclwwlk2lem1lem  30370  extwwlkfab  30380  frgrreggt1  30421  ubthlem1  30898  norm-i  31157  hoeq  31788  nmopgt0  31940  pjimai  32204  chirredi  32422  addltmulALT  32474  bian1d  32483  opreu2reuALT  32504  sbcies  32515  rmounid  32522  iunrdx  32583  disjrdx  32610  cnvoprabOLD  32737  archiabl  33187  islbs5  33387  ist0cld  33793  oms0  34278  eulerpartgbij  34353  sgnneg  34521  sgn3da  34522  reprinrn  34611  usgrgt2cycl  35114  satfv1lem  35346  satf0op  35361  dmopab3rexdif  35389  satefvfmla0  35402  mrsubrn  35497  topfne  36336  unbdqndv1  36490  bj-hbntbi  36686  bj-issetwt  36857  bj-clel3gALT  37030  copsex2d  37121  bj-elid6  37152  dfgcd3  37306  topdifinfeq  37332  wl-sbalnae  37542  sin2h  37596  poimirlem16  37622  poimirlem17  37623  poimirlem25  37631  mbfresfi  37652  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  ftc1anclem1  37679  isidlc  38001  eldmressnALTV  38253  islshpsm  38961  lshpkrlem1  39091  opcon1b  39179  lautlt  40073  lauteq  40077  idlaut  40078  diblsmopel  41153  doch11  41355  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  metakunt16  42201  f1o2d2  42252  dvdsexpnn0  42347  redvmptabs  42368  prjsprellsp  42597  prjspeclsp  42598  abbibw  42663  istopclsd  42687  eqrabdioph  42764  rexzrexnn0  42791  zindbi  42934  expdiophlem2  43010  onsupeqmax  43234  onsupeqnmax  43235  ordeldif  43247  infordmin  43521  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  sqrtcvallem1  43620  reabsifneg  43621  fsovrfovd  43998  ntrclsiso  44056  ntrneifv3  44071  ntrneineine0lem  44072  ntrneicls11  44079  suprleubrd  44155  suprlubrd  44157  lemuldiv4d  44160  pm14.122a  44417  3impexpbicomi  44477  onfrALTlem5  44539  bitr3VD  44846  onfrALTlem5VD  44882  csbrngVD  44893  pwpwuni  44996  supxrre3  45274  xrralrecnnge  45339  eliooshift  45458  limsupre2lem  45679  liminflimsupclim  45762  xlimbr  45782  smfrec  46744  fsetprcnexALT  47011  f1cof1b  47026  reuf1odnf  47056  2reuimp  47064  ralbinrald  47071  afvco2  47125  dfatdmfcoafv2  47203  recnmulnred  47254  sqrtnegnre  47256  subsubelfzo0  47275  ichcircshi  47378  sprvalpwle2  47413  sprsymrelf1lem  47415  sbcpr  47445  poprelb  47448  31prm  47521  requad01  47545  dfeven3  47582  iseven5  47588  0noddALTV  47613  2noddALTV  47617  fpprmod  47651  sbgoldbaltlem1  47703  bgoldbtbndlem2  47730  dfclnbgr2  47747  dfsclnbgr2  47769  dfvopnbgr2  47776  dfsclnbgr6  47781  isuspgrim0lem  47808  usgrgrtrirex  47852  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  0nodd  48013  2nodd  48015  isassintop  48053  uzlidlring  48078  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  nn0sumltlt  48194  ply1mulgsumlem2  48232  islindeps  48298  lindslinindsimp1  48302  lindslinindsimp2  48308  snlindsntor  48316  zlmodzxznm  48342  ldepslinc  48354  difmodm1lt  48371  elbigo2  48401  elbigolo1  48406  logblt1b  48413  fldivexpfllog2  48414  nnolog2flm1  48439  digexp  48456  nn0sumshdiglemB  48469  itsclquadeu  48626  itscnhlinecirc02p  48634  ipolublem  48774  ipoglblem  48777