Theorem bicomd 222

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 221	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  impbid2  225  syl5ibr  245  ibir  267  bitr2d  279  bitr3d  280  bitr4d  281  bitr2id  284  bitr2di  288  con1bid  356  pm5.5  362  imnot  366  baibr  537  rbaib  539  baibd  540  anabs5  660  annotanannot  832  pm5.55  946  pm5.54  1015  ninba  1019  pm5.75  1026  norassOLD  1536  sbequ12r  2246  sbal1  2534  euor2  2616  abbi1dv  2879  necon3bbid  2982  necon4bbid  2986  ralanid  3095  rexanid  3184  ralcom2  3291  sbralie  3407  rabrabi  3428  rabeqcda  3430  gencbvex  3489  sbhypf  3492  alexeqg  3582  clel2g  3589  clel2gOLD  3590  clel3g  3592  clel4g  3594  reu8  3669  sbceq2a  3729  sbcco2  3744  reu8nf  3811  notabw  4238  2reu4lem  4457  reurexprg  4641  raltpd  4718  ssdifsn  4722  uniprg  4857  disjxun  5073  opabidw  5438  opabid  5439  soeq2  5526  posn  5673  xpiindi  5747  dmopab2rex  5829  elpredg  6220  fvopab6  6917  cbvfo  7170  f1eqcocnv  7182  f1eqcocnvOLD  7183  isoid  7209  isoini  7218  isosolem  7227  riotaeqimp  7268  resoprab2  7402  tfisi  7714  tfinds2  7719  f1oweALT  7824  dfoprab3  7903  opiota  7908  mpocurryd  8094  oalimcl  8400  omword  8410  oeword  8430  nnacan  8468  nnmcan  8474  mapsnd  8683  findcard2s  8957  funisfsupp  9142  suppeqfsuppbi  9151  eqinf  9252  inflb  9257  infglb  9258  infglbb  9259  infltoreq  9270  infempty  9275  brwdomn0  9337  cantnfp1lem3  9447  ssrankr1  9602  r1pw  9612  djulf1o  9679  djurf1o  9680  aleph11  9849  alephval3  9875  gch-kn  10442  wunex2  10503  lttri2  11066  wloglei  11516  divne0b  11653  lemul1  11836  nnnle0  12015  div4p1lem1div2  12237  nn0ind-raph  12429  zindd  12430  suprfinzcl  12445  rebtwnz  12696  qreccl  12718  elpq  12724  xrlttri2  12885  2resupmax  12931  xmulneg1  13012  iooshf  13167  difreicc  13225  fzofzim  13443  elfzomelpfzo  13500  elfznelfzo  13501  zmodid2  13628  2submod  13661  modfzo0difsn  13672  om2uzlti  13679  expcan  13896  hashvnfin  14084  hashneq0  14088  prhash2ex  14123  hashgt0elex  14125  hashgt12el  14146  hashgt12el2  14147  hashbclem  14173  hashf1lem2  14179  prprrab  14196  swrd0  14380  pfxn0  14408  swrdswrd  14427  pfxccat3  14456  repswswrd  14506  cshf1  14532  cshw1repsw  14545  relexpindlem  14783  absz  15032  iserex  15377  prodrb  15651  absdvdsb  15993  dvdsabsb  15994  modmulconst  16006  dvdsadd  16020  dvdsabseq  16031  mod2eq0even  16064  oddnn02np1  16066  oddge22np1  16067  evennn02n  16068  evennn2n  16069  zeo5  16074  sadadd2lem2  16166  smupvallem  16199  gcdass  16264  lcmdvds  16322  lcmass  16328  divgcdcoprm0  16379  divgcdcoprmex  16380  1nprm  16393  dvdsnprmd  16404  prmdvdssq  16432  ncoprmlnprm  16441  isevengcd2  16443  m1dvdsndvds  16508  cshws0  16812  sbcie2s  16871  sbcie3s  16872  dfiso2  17493  initoid  17725  termoid  17726  funcestrcsetclem8  17873  lublecllem  18087  odudlatb  18252  issubm2  18452  mgm2nsgrplem2  18567  nsgacs  18799  cycsubg2  18838  gapm  18921  sscntz  18941  pgrpsubgsymgbi  19025  f1omvdcnv  19061  pmtrprfvalrn  19105  odval2  19168  lsmcntz  19294  rhmf1o  19985  isrim  19986  dfprm2  20704  psgnfix2  20813  islinds3  21050  islindf4  21054  snifpsrbag  21134  gsumply1eq  21485  mdetdiaglem  21756  mdetunilem9  21778  slesolinv  21838  slesolex  21840  cpmatel2  21871  m2cpmghm  21902  m2cpminvid2  21913  pm2mpf1  21957  chfacfscmul0  22016  chfacfscmulfsupp  22017  chfacfpmmul0  22020  chfacfpmmulfsupp  22021  isopn2  22192  cmpsub  22560  connsub  22581  ncvs1  24330  rrxmvallem  24577  itg1mulc  24878  lhop1  25187  mdegleb  25238  lawcos  25975  leibpi  26101  2lgslem1a  26548  2sq2  26590  iscgra  27179  colinearalg  27287  edg0iedg0  27434  uhgreq12g  27444  uhgrvtxedgiedgb  27515  usgredg2v  27603  edg0usgr  27629  dfnbgr2  27713  nbuhgr  27719  nbusgredgeu0  27744  nb3grprlem1  27756  nb3grpr  27758  uvtx2vtx1edgb  27775  redwlk  28049  uhgrwkspthlem2  28131  usgr2wlkspth  28136  pthdlem1  28143  cyclnspth  28177  crctcshwlkn0lem1  28184  crctcshwlkn0lem4  28187  crctcsh  28198  iswwlksnx  28214  wwlksm1edg  28255  wwlksnextsurj  28274  wwlksnextproplem3  28285  2wlkdlem4  28302  2wlkdlem5  28303  2pthdlem1  28304  s3wwlks2on  28330  wpthswwlks2on  28335  elwspths2spth  28341  rusgrnumwwlks  28348  umgrclwwlkge2  28364  clwlkclwwlklem2a4  28370  clwlkclwwlk  28375  clwlkclwwlkflem  28377  clwwisshclwws  28388  isclwwlknx  28409  clwwlknwwlksnb  28428  eclclwwlkn1  28448  clwwlknonel  28468  clwwlknun  28485  3wlkdlem6  28538  frgrncvvdeqlem9  28680  fusgreg2wsp  28709  numclwwlk2lem1lem  28715  extwwlkfab  28725  frgrreggt1  28766  ubthlem1  29241  norm-i  29500  hoeq  30131  nmopgt0  30283  pjimai  30547  chirredi  30765  addltmulALT  30817  opreu2reuALT  30834  sbcies  30845  rmounid  30852  iunrdx  30912  disjrdx  30939  cnvoprabOLD  31064  archiabl  31461  ist0cld  31792  oms0  32273  eulerpartgbij  32348  sgnneg  32516  sgn3da  32517  reprinrn  32607  usgrgt2cycl  33101  satfv1lem  33333  satf0op  33348  dmopab3rexdif  33376  satefvfmla0  33389  mrsubrn  33484  riotarab  33682  reurab  33683  sotrine  33743  xpord2ind  33803  xpord3ind  33809  topfne  34552  unbdqndv1  34697  bj-hbntbi  34895  bj-issetwt  35068  bj-clel3gALT  35230  copsex2d  35319  bj-elid6  35350  dfgcd3  35504  topdifinfeq  35530  wl-sb6rft  35712  wl-sbalnae  35726  sin2h  35776  poimirlem16  35802  poimirlem17  35803  poimirlem25  35811  mbfresfi  35832  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  ftc1anclem1  35859  isidlc  36182  islshpsm  37001  lshpkrlem1  37131  opcon1b  37219  lautlt  38112  lauteq  38116  idlaut  38117  diblsmopel  39192  doch11  39394  recbothd  40008  aks4d1p8d2  40100  aks4d1p8  40102  sticksstones1  40109  sticksstones11  40119  sticksstones22  40131  metakunt16  40147  dvdsexpnn0  40348  prjsprellsp  40457  prjspeclsp  40458  istopclsd  40529  eqrabdioph  40606  rexzrexnn0  40633  zindbi  40775  expdiophlem2  40851  infordmin  41146  inintabd  41194  cnvcnvintabd  41215  cnvintabd  41218  sqrtcvallem1  41246  reabsifneg  41247  fsovrfovd  41624  ntrclsiso  41684  ntrneifv3  41699  ntrneineine0lem  41700  ntrneicls11  41707  suprleubrd  41784  suprlubrd  41786  lemuldiv4d  41789  pm14.122a  42047  3impexpbicomi  42107  onfrALTlem5  42169  bitr3VD  42476  onfrALTlem5VD  42512  csbrngVD  42523  pwpwuni  42612  supxrre3  42871  xrralrecnnge  42937  eliooshift  43051  limsupre2lem  43272  liminflimsupclim  43355  xlimbr  43375  smfrec  44334  fsetprcnexALT  44567  f1cof1b  44580  reuf1odnf  44610  2reuimp  44618  ralbinrald  44625  afvco2  44679  dfatdmfcoafv2  44757  recnmulnred  44808  sqrtnegnre  44810  subsubelfzo0  44829  ichcircshi  44917  sprvalpwle2  44952  sprsymrelf1lem  44954  sbcpr  44984  poprelb  44987  31prm  45060  requad01  45084  dfeven3  45121  iseven5  45127  0noddALTV  45152  2noddALTV  45156  fpprmod  45190  sbgoldbaltlem1  45242  bgoldbtbndlem2  45269  isomuspgrlem2d  45294  0nodd  45375  2nodd  45377  isassintop  45415  rnghmf1o  45472  isrngim  45473  uzlidlring  45498  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  nn0sumltlt  45697  ply1mulgsumlem2  45739  islindeps  45805  lindslinindsimp1  45809  lindslinindsimp2  45815  snlindsntor  45823  zlmodzxznm  45849  ldepslinc  45861  difmodm1lt  45879  elbigo2  45909  elbigolo1  45914  logblt1b  45921  fldivexpfllog2  45922  nnolog2flm1  45947  digexp  45964  nn0sumshdiglemB  45977  itsclquadeu  46134  itscnhlinecirc02p  46142  ipolublem  46283  ipoglblem  46286