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  imbitrrid  245  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  660  annotanannot  832  pm5.55  946  pm5.54  1015  ninba  1019  pm5.75  1026  sbequ12r  2243  sbal1  2526  euor2  2608  eqabcdv  2867  necon3bbid  2977  necon4bbid  2981  ralanid  3094  rexanid  3095  sbralieALT  3354  ralcom2  3372  rmoanid  3385  reuanid  3386  rabrabi  3449  gencbvex  3535  sbhypfOLD  3539  alexeqg  3639  clel2g  3647  clel2gOLD  3648  clel3g  3650  clel4g  3652  reurab  3697  reu8  3729  sbceq2a  3789  sbcco2  3804  reu8nf  3871  notabw  4303  2reu4lem  4525  reurexprg  4708  raltpd  4785  ssdifsn  4791  uniprg  4925  disjxun  5146  opabidw  5524  opabid  5525  soeq2  5610  sotrine  5626  posn  5761  xpiindi  5835  dmopab2rex  5917  elpredg  6314  fvopab6  7031  cbvfo  7290  f1eqcocnv  7302  f1eqcocnvOLD  7303  isoid  7329  isoini  7338  isosolem  7347  riotaeqimp  7395  riotarab  7411  resoprab2  7530  tfisi  7852  tfinds2  7857  f1oweALT  7963  dfoprab3  8044  opiota  8049  xpord2indlem  8138  xpord3inddlem  8145  mpocurryd  8260  oalimcl  8566  omword  8576  oeword  8596  nnacan  8634  nnmcan  8640  mapsnd  8886  findcard2s  9171  funisfsupp  9373  suppeqfsuppbi  9383  eqinf  9485  inflb  9490  infglb  9491  infglbb  9492  infltoreq  9503  infempty  9508  brwdomn0  9570  cantnfp1lem3  9681  ssrankr1  9836  r1pw  9846  djulf1o  9913  djurf1o  9914  aleph11  10085  alephval3  10111  gch-kn  10678  wunex2  10739  lttri2  11303  wloglei  11753  divne0b  11890  lemul1  12073  nnnle0  12252  div4p1lem1div2  12474  nn0ind-raph  12669  zindd  12670  suprfinzcl  12683  rebtwnz  12938  qreccl  12960  elpq  12966  xrlttri2  13128  2resupmax  13174  xmulneg1  13255  iooshf  13410  difreicc  13468  fzofzim  13686  elfzomelpfzo  13743  elfznelfzo  13744  zmodid2  13871  2submod  13904  modfzo0difsn  13915  om2uzlti  13922  expcan  14141  hashvnfin  14327  hashneq0  14331  prhash2ex  14366  hashgt0elex  14368  hashgt12el  14389  hashgt12el2  14390  hashbclem  14418  hashf1lem2  14424  prprrab  14441  swrd0  14615  pfxn0  14643  swrdswrd  14662  pfxccat3  14691  repswswrd  14741  cshf1  14767  cshw1repsw  14780  relexpindlem  15017  absz  15265  iserex  15610  prodrb  15883  absdvdsb  16225  dvdsabsb  16226  modmulconst  16238  dvdsadd  16252  dvdsabseq  16263  mod2eq0even  16296  oddnn02np1  16298  oddge22np1  16299  evennn02n  16300  evennn2n  16301  zeo5  16306  sadadd2lem2  16398  smupvallem  16431  gcdass  16496  lcmdvds  16552  lcmass  16558  divgcdcoprm0  16609  divgcdcoprmex  16610  1nprm  16623  dvdsnprmd  16634  prmdvdssq  16662  ncoprmlnprm  16671  isevengcd2  16673  m1dvdsndvds  16738  cshws0  17042  sbcie3s  17102  dfiso2  17726  initoid  17961  termoid  17962  funcestrcsetclem8  18109  lublecllem  18323  odudlatb  18488  sgrppropd  18662  issubm2  18727  mgm2nsgrplem2  18842  nsgacs  19085  cycsubg2  19132  gapm  19218  sscntz  19238  pgrpsubgsymgbi  19324  f1omvdcnv  19360  pmtrprfvalrn  19404  odval2  19467  lsmcntz  19595  rngpropd  20075  rnghmf1o  20350  isrngim2  20351  rhmf1o  20389  isrim  20390  isrimOLD  20391  dfprm2  21333  pzriprnglem10  21350  psgnfix2  21462  islinds3  21699  islindf4  21703  snifpsrbag  21785  gsumply1eq  22149  mdetdiaglem  22420  mdetunilem9  22442  slesolinv  22502  slesolex  22504  cpmatel2  22535  m2cpmghm  22566  m2cpminvid2  22577  pm2mpf1  22621  chfacfscmul0  22680  chfacfscmulfsupp  22681  chfacfpmmul0  22684  chfacfpmmulfsupp  22685  isopn2  22856  cmpsub  23224  connsub  23245  ncvs1  25005  rrxmvallem  25252  itg1mulc  25554  lhop1  25867  mdegleb  25920  lawcos  26662  leibpi  26788  2lgslem1a  27238  2sq2  27280  sletric  27611  0reno  28106  colinearalg  28602  edg0iedg0  28749  uhgreq12g  28759  uhgrvtxedgiedgb  28830  usgredg2v  28918  edg0usgr  28944  dfnbgr2  29028  nbuhgr  29034  nbusgredgeu0  29059  nb3grprlem1  29071  nb3grpr  29073  uvtx2vtx1edgb  29090  redwlk  29363  uhgrwkspthlem2  29445  usgr2wlkspth  29450  pthdlem1  29457  cyclnspth  29491  crctcshwlkn0lem1  29498  crctcshwlkn0lem4  29501  crctcsh  29512  iswwlksnx  29528  wwlksm1edg  29569  wwlksnextsurj  29588  wwlksnextproplem3  29599  2wlkdlem4  29616  2wlkdlem5  29617  2pthdlem1  29618  s3wwlks2on  29644  wpthswwlks2on  29649  elwspths2spth  29655  rusgrnumwwlks  29662  umgrclwwlkge2  29678  clwlkclwwlklem2a4  29684  clwlkclwwlk  29689  clwlkclwwlkflem  29691  clwwisshclwws  29702  isclwwlknx  29723  clwwlknwwlksnb  29742  eclclwwlkn1  29762  clwwlknonel  29782  clwwlknun  29799  3wlkdlem6  29852  frgrncvvdeqlem9  29994  fusgreg2wsp  30023  numclwwlk2lem1lem  30029  extwwlkfab  30039  frgrreggt1  30080  ubthlem1  30557  norm-i  30816  hoeq  31447  nmopgt0  31599  pjimai  31863  chirredi  32081  addltmulALT  32133  opreu2reuALT  32151  sbcies  32162  rmounid  32169  iunrdx  32229  disjrdx  32256  cnvoprabOLD  32379  archiabl  32781  islbs5  32937  ist0cld  33278  oms0  33761  eulerpartgbij  33836  sgnneg  34004  sgn3da  34005  reprinrn  34095  usgrgt2cycl  34586  satfv1lem  34818  satf0op  34833  dmopab3rexdif  34861  satefvfmla0  34874  mrsubrn  34969  gg-cncrng  35649  topfne  35705  unbdqndv1  35850  bj-hbntbi  36048  bj-issetwt  36220  bj-clel3gALT  36395  copsex2d  36486  bj-elid6  36517  dfgcd3  36671  topdifinfeq  36697  wl-sb6rft  36879  wl-sbalnae  36893  sin2h  36944  poimirlem16  36970  poimirlem17  36971  poimirlem25  36979  mbfresfi  37000  itg2addnclem  37005  itg2addnclem2  37006  itg2addnclem3  37007  ftc1anclem1  37027  isidlc  37349  eldmressnALTV  37606  islshpsm  38316  lshpkrlem1  38446  opcon1b  38534  lautlt  39428  lauteq  39432  idlaut  39433  diblsmopel  40508  doch11  40710  recbothd  41327  aks4d1p8d2  41419  aks4d1p8  41421  sticksstones1  41431  sticksstones11  41441  sticksstones22  41453  metakunt16  41469  f1o2d2  41524  dvdsexpnn0  41697  prjsprellsp  41818  prjspeclsp  41819  istopclsd  41903  eqrabdioph  41980  rexzrexnn0  42007  zindbi  42150  expdiophlem2  42226  onsupeqmax  42460  onsupeqnmax  42461  ordeldif  42473  infordmin  42748  inintabd  42795  cnvcnvintabd  42816  cnvintabd  42819  sqrtcvallem1  42847  reabsifneg  42848  fsovrfovd  43225  ntrclsiso  43283  ntrneifv3  43298  ntrneineine0lem  43299  ntrneicls11  43306  suprleubrd  43383  suprlubrd  43385  lemuldiv4d  43388  pm14.122a  43646  3impexpbicomi  43706  onfrALTlem5  43768  bitr3VD  44075  onfrALTlem5VD  44111  csbrngVD  44122  pwpwuni  44208  supxrre3  44496  xrralrecnnge  44561  eliooshift  44680  limsupre2lem  44901  liminflimsupclim  44984  xlimbr  45004  smfrec  45966  fsetprcnexALT  46233  f1cof1b  46246  reuf1odnf  46276  2reuimp  46284  ralbinrald  46291  afvco2  46345  dfatdmfcoafv2  46423  recnmulnred  46474  sqrtnegnre  46476  subsubelfzo0  46495  ichcircshi  46583  sprvalpwle2  46618  sprsymrelf1lem  46620  sbcpr  46650  poprelb  46653  31prm  46726  requad01  46750  dfeven3  46787  iseven5  46793  0noddALTV  46818  2noddALTV  46822  fpprmod  46856  sbgoldbaltlem1  46908  bgoldbtbndlem2  46935  isomuspgrlem2d  46960  0nodd  47009  2nodd  47011  isassintop  47049  uzlidlring  47074  funcringcsetcALTV2lem8  47136  funcringcsetclem8ALTV  47159  nn0sumltlt  47191  ply1mulgsumlem2  47232  islindeps  47298  lindslinindsimp1  47302  lindslinindsimp2  47308  snlindsntor  47316  zlmodzxznm  47342  ldepslinc  47354  difmodm1lt  47372  elbigo2  47402  elbigolo1  47407  logblt1b  47414  fldivexpfllog2  47415  nnolog2flm1  47440  digexp  47457  nn0sumshdiglemB  47470  itsclquadeu  47627  itscnhlinecirc02p  47635  ipolublem  47775  ipoglblem  47778