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  283  bitr2di  287  con1bid  355  pm5.5  361  imnot  365  baibr  536  rbaib  538  baibd  539  anabs5  659  annotanannot  831  pm5.55  945  pm5.54  1014  ninba  1018  pm5.75  1025  norassOLD  1536  sbequ12r  2248  sbal1  2533  euor2  2615  abbi1dv  2877  necon3bbid  2980  necon4bbid  2984  ralanid  3093  rexanid  3182  ralcom2  3288  sbralie  3395  rabrabi  3417  rabeqcda  3419  gencbvex  3478  sbhypf  3481  alexeqg  3573  clel2g  3581  clel2gOLD  3582  clel3g  3584  clel4g  3586  reu8  3663  sbceq2a  3723  sbcco2  3738  reu8nf  3806  notabw  4234  2reu4lem  4453  reurexprg  4637  raltpd  4714  ssdifsn  4718  uniprg  4853  disjxun  5068  opabidw  5431  opabid  5432  soeq2  5516  posn  5663  xpiindi  5733  dmopab2rex  5815  elpredg  6205  fvopab6  6890  cbvfo  7141  f1eqcocnv  7153  f1eqcocnvOLD  7154  isoid  7180  isoini  7189  isosolem  7198  riotaeqimp  7239  resoprab2  7371  tfisi  7680  tfinds2  7685  f1oweALT  7788  dfoprab3  7867  opiota  7872  mpocurryd  8056  oalimcl  8353  omword  8363  oeword  8383  nnacan  8421  nnmcan  8427  mapsnd  8632  findcard2s  8910  funisfsupp  9063  suppeqfsuppbi  9072  eqinf  9173  inflb  9178  infglb  9179  infglbb  9180  infltoreq  9191  infempty  9196  brwdomn0  9258  cantnfp1lem3  9368  ssrankr1  9524  r1pw  9534  djulf1o  9601  djurf1o  9602  aleph11  9771  alephval3  9797  gch-kn  10364  wunex2  10425  lttri2  10988  wloglei  11437  divne0b  11574  lemul1  11757  nnnle0  11936  div4p1lem1div2  12158  nn0ind-raph  12350  zindd  12351  suprfinzcl  12365  rebtwnz  12616  qreccl  12638  elpq  12644  xrlttri2  12805  2resupmax  12851  xmulneg1  12932  iooshf  13087  difreicc  13145  fzofzim  13362  elfzomelpfzo  13419  elfznelfzo  13420  zmodid2  13547  2submod  13580  modfzo0difsn  13591  om2uzlti  13598  expcan  13815  hashvnfin  14003  hashneq0  14007  prhash2ex  14042  hashgt0elex  14044  hashgt12el  14065  hashgt12el2  14066  hashbclem  14092  hashf1lem2  14098  prprrab  14115  swrd0  14299  pfxn0  14327  swrdswrd  14346  pfxccat3  14375  repswswrd  14425  cshf1  14451  cshw1repsw  14464  relexpindlem  14702  absz  14951  iserex  15296  prodrb  15570  absdvdsb  15912  dvdsabsb  15913  modmulconst  15925  dvdsadd  15939  dvdsabseq  15950  mod2eq0even  15983  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  zeo5  15993  sadadd2lem2  16085  smupvallem  16118  gcdass  16183  lcmdvds  16241  lcmass  16247  divgcdcoprm0  16298  divgcdcoprmex  16299  1nprm  16312  dvdsnprmd  16323  prmdvdssq  16351  ncoprmlnprm  16360  isevengcd2  16362  m1dvdsndvds  16427  cshws0  16731  sbcie2s  16790  sbcie3s  16791  dfiso2  17401  initoid  17632  termoid  17633  funcestrcsetclem8  17780  lublecllem  17993  odudlatb  18158  issubm2  18358  mgm2nsgrplem2  18473  nsgacs  18705  cycsubg2  18744  gapm  18827  sscntz  18847  pgrpsubgsymgbi  18931  f1omvdcnv  18967  pmtrprfvalrn  19011  odval2  19074  lsmcntz  19200  rhmf1o  19891  isrim  19892  dfprm2  20607  psgnfix2  20716  islinds3  20951  islindf4  20955  snifpsrbag  21035  gsumply1eq  21386  mdetdiaglem  21655  mdetunilem9  21677  slesolinv  21737  slesolex  21739  cpmatel2  21770  m2cpmghm  21801  m2cpminvid2  21812  pm2mpf1  21856  chfacfscmul0  21915  chfacfscmulfsupp  21916  chfacfpmmul0  21919  chfacfpmmulfsupp  21920  isopn2  22091  cmpsub  22459  connsub  22480  ncvs1  24226  rrxmvallem  24473  itg1mulc  24774  lhop1  25083  mdegleb  25134  lawcos  25871  leibpi  25997  2lgslem1a  26444  2sq2  26486  iscgra  27074  colinearalg  27181  edg0iedg0  27328  uhgreq12g  27338  uhgrvtxedgiedgb  27409  usgredg2v  27497  edg0usgr  27523  dfnbgr2  27607  nbuhgr  27613  nbusgredgeu0  27638  nb3grprlem1  27650  nb3grpr  27652  uvtx2vtx1edgb  27669  redwlk  27942  uhgrwkspthlem2  28023  usgr2wlkspth  28028  pthdlem1  28035  cyclnspth  28069  crctcshwlkn0lem1  28076  crctcshwlkn0lem4  28079  crctcsh  28090  iswwlksnx  28106  wwlksm1edg  28147  wwlksnextsurj  28166  wwlksnextproplem3  28177  2wlkdlem4  28194  2wlkdlem5  28195  2pthdlem1  28196  s3wwlks2on  28222  wpthswwlks2on  28227  elwspths2spth  28233  rusgrnumwwlks  28240  umgrclwwlkge2  28256  clwlkclwwlklem2a4  28262  clwlkclwwlk  28267  clwlkclwwlkflem  28269  clwwisshclwws  28280  isclwwlknx  28301  clwwlknwwlksnb  28320  eclclwwlkn1  28340  clwwlknonel  28360  clwwlknun  28377  3wlkdlem6  28430  frgrncvvdeqlem9  28572  fusgreg2wsp  28601  numclwwlk2lem1lem  28607  extwwlkfab  28617  frgrreggt1  28658  ubthlem1  29133  norm-i  29392  hoeq  30023  nmopgt0  30175  pjimai  30439  chirredi  30657  addltmulALT  30709  opreu2reuALT  30726  sbcies  30737  rmounid  30744  iunrdx  30804  disjrdx  30831  cnvoprabOLD  30957  archiabl  31354  ist0cld  31685  oms0  32164  eulerpartgbij  32239  sgnneg  32407  sgn3da  32408  reprinrn  32498  usgrgt2cycl  32992  satfv1lem  33224  satf0op  33239  dmopab3rexdif  33267  satefvfmla0  33280  mrsubrn  33375  riotarab  33575  reurab  33576  sotrine  33640  xpord2ind  33721  xpord3ind  33727  topfne  34470  unbdqndv1  34615  bj-hbntbi  34813  bj-issetwt  34986  bj-clel3gALT  35148  copsex2d  35237  bj-elid6  35268  dfgcd3  35422  topdifinfeq  35448  wl-sb6rft  35630  wl-sbalnae  35644  sin2h  35694  poimirlem16  35720  poimirlem17  35721  poimirlem25  35729  mbfresfi  35750  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  ftc1anclem1  35777  isidlc  36100  islshpsm  36921  lshpkrlem1  37051  opcon1b  37139  lautlt  38032  lauteq  38036  idlaut  38037  diblsmopel  39112  doch11  39314  recbothd  39929  aks4d1p8d2  40021  aks4d1p8  40023  sticksstones1  40030  sticksstones11  40040  sticksstones22  40052  metakunt16  40068  dvdsexpnn0  40262  prjsprellsp  40371  prjspeclsp  40372  istopclsd  40438  eqrabdioph  40515  rexzrexnn0  40542  zindbi  40684  expdiophlem2  40760  infordmin  41037  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  sqrtcvallem1  41128  reabsifneg  41129  fsovrfovd  41506  ntrclsiso  41566  ntrneifv3  41581  ntrneineine0lem  41582  ntrneicls11  41589  suprleubrd  41666  suprlubrd  41668  lemuldiv4d  41671  pm14.122a  41929  3impexpbicomi  41989  onfrALTlem5  42051  bitr3VD  42358  onfrALTlem5VD  42394  csbrngVD  42405  pwpwuni  42494  supxrre3  42754  xrralrecnnge  42820  eliooshift  42934  limsupre2lem  43155  liminflimsupclim  43238  xlimbr  43258  smfrec  44210  fsetprcnexALT  44443  f1cof1b  44456  reuf1odnf  44486  2reuimp  44494  ralbinrald  44501  afvco2  44555  dfatdmfcoafv2  44633  recnmulnred  44685  sqrtnegnre  44687  subsubelfzo0  44706  ichcircshi  44794  sprvalpwle2  44829  sprsymrelf1lem  44831  sbcpr  44861  poprelb  44864  31prm  44937  requad01  44961  dfeven3  44998  iseven5  45004  0noddALTV  45029  2noddALTV  45033  fpprmod  45067  sbgoldbaltlem1  45119  bgoldbtbndlem2  45146  isomuspgrlem2d  45171  0nodd  45252  2nodd  45254  isassintop  45292  rnghmf1o  45349  isrngim  45350  uzlidlring  45375  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  nn0sumltlt  45574  ply1mulgsumlem2  45616  islindeps  45682  lindslinindsimp1  45686  lindslinindsimp2  45692  snlindsntor  45700  zlmodzxznm  45726  ldepslinc  45738  difmodm1lt  45756  elbigo2  45786  elbigolo1  45791  logblt1b  45798  fldivexpfllog2  45799  nnolog2flm1  45824  digexp  45841  nn0sumshdiglemB  45854  itsclquadeu  46011  itscnhlinecirc02p  46019  ipolublem  46160  ipoglblem  46163