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  664  annotanannot  835  pm5.55  951  pm5.54  1020  ninba  1024  pm5.75  1031  sbequ12r  2260  sbal1  2533  euor2  2614  eqabcdv  2871  necon3bbid  2970  necon4bbid  2974  ralanid  3086  rexanid  3087  sbralieALT  3317  ralcom2  3340  rmoanid  3353  reuanid  3354  rabrabi  3409  gencbvex  3488  alexeqg  3594  clel2g  3602  clel3g  3604  clel4g  3606  reurab  3648  reu8  3680  sbceq2a  3741  sbcco2  3756  reu8nf  3816  notabw  4254  2reu4lem  4464  reurexprg  4649  raltpd  4726  ssdifsn  4732  uniprg  4867  disjxun  5084  opabidw  5473  opabid  5474  soeq2  5555  sotrine  5573  posn  5711  xpiindi  5785  dmopab2rex  5867  elpredg  6274  fvopab6  6977  cbvfo  7238  f1eqcocnv  7250  isoid  7278  isoini  7287  isosolem  7296  riotaeqimp  7344  riotarab  7360  resoprab2  7480  tfisi  7804  tfinds2  7809  f1oweALT  7919  dfoprab3  8001  opiota  8006  xpord2indlem  8091  xpord3inddlem  8098  mpocurryd  8213  oalimcl  8489  omword  8499  oeword  8520  nnacan  8558  nnmcan  8564  mapsnd  8828  findcard2s  9094  funisfsupp  9274  suppeqfsuppbi  9286  eqinf  9392  inflb  9397  infglb  9398  infglbb  9399  infltoreq  9411  infempty  9416  brwdomn0  9478  cantnfp1lem3  9595  ssrankr1  9753  r1pw  9763  djulf1o  9830  djurf1o  9831  aleph11  10000  alephval3  10026  gch-kn  10594  wunex2  10655  lttri2  11222  wloglei  11676  divne0b  11814  lemul1  12001  nnnle0  12204  div4p1lem1div2  12426  nn0ind-raph  12623  zindd  12624  suprfinzcl  12637  rebtwnz  12891  qreccl  12913  elpq  12919  xrlttri2  13087  2resupmax  13134  xmulneg1  13215  iooshf  13373  difreicc  13431  fzofzim  13658  elfzomelpfzo  13721  elfznelfzo  13722  zmodid2  13852  2submod  13888  modfzo0difsn  13899  om2uzlti  13906  expcan  14125  hashvnfin  14316  hashneq0  14320  prhash2ex  14355  hashgt0elex  14357  hashgt12el  14378  hashgt12el2  14379  hashbclem  14408  hashf1lem2  14412  prprrab  14429  swrd0  14615  pfxn0  14643  swrdswrd  14661  pfxccat3  14690  repswswrd  14740  cshf1  14766  cshw1repsw  14779  relexpindlem  15019  absz  15267  iserex  15613  prodrb  15891  absdvdsb  16237  dvdsabsb  16238  modmulconst  16251  dvdsadd  16265  dvdsabseq  16276  mod2eq0even  16309  oddnn02np1  16311  oddge22np1  16312  evennn02n  16313  evennn2n  16314  zeo5  16319  sadadd2lem2  16413  smupvallem  16446  gcdass  16510  lcmdvds  16571  lcmass  16577  divgcdcoprm0  16628  divgcdcoprmex  16629  1nprm  16642  dvdsnprmd  16653  prmdvdssq  16682  ncoprmlnprm  16692  isevengcd2  16694  m1dvdsndvds  16763  cshws0  17066  sbcie3s  17126  dfiso2  17733  initoid  17962  termoid  17963  funcestrcsetclem8  18107  lublecllem  18318  odudlatb  18485  sgrppropd  18693  issubm2  18766  mgm2nsgrplem2  18884  nsgacs  19131  cycsubg2  19179  gapm  19275  sscntz  19295  pgrpsubgsymgbi  19377  f1omvdcnv  19413  pmtrprfvalrn  19457  odval2  19520  lsmcntz  19648  rngpropd  20149  rnghmf1o  20426  isrngim2  20427  rhmf1o  20464  isrim  20465  dfprm2  21466  pzriprnglem10  21483  psgnfix2  21592  islinds3  21827  islindf4  21831  snifpsrbag  21913  gsumply1eq  22287  mdetdiaglem  22576  mdetunilem9  22598  slesolinv  22658  slesolex  22660  cpmatel2  22691  m2cpmghm  22722  m2cpminvid2  22733  pm2mpf1  22777  chfacfscmul0  22836  chfacfscmulfsupp  22837  chfacfpmmul0  22840  chfacfpmmulfsupp  22841  isopn2  23010  cmpsub  23378  connsub  23399  ncvs1  25137  rrxmvallem  25384  itg1mulc  25684  lhop1  25994  mdegleb  26042  lawcos  26796  leibpi  26922  2lgslem1a  27371  2sq2  27413  lestric  27749  bdayons  28285  n0subs2  28373  bdaypw2n0bndlem  28472  colinearalg  28996  edg0iedg0  29141  uhgreq12g  29151  uhgrvtxedgiedgb  29222  usgredg2v  29313  edg0usgr  29339  dfnbgr2  29423  nbuhgr  29429  nbusgredgeu0  29454  nb3grprlem1  29466  nb3grpr  29468  uvtx2vtx1edgb  29485  redwlk  29757  uhgrwkspthlem2  29840  usgr2wlkspth  29845  pthdlem1  29852  cyclnspth  29887  crctcshwlkn0lem1  29896  crctcshwlkn0lem4  29899  crctcsh  29910  iswwlksnx  29926  wwlksm1edg  29967  wwlksnextsurj  29986  wwlksnextproplem3  29997  2wlkdlem4  30014  2wlkdlem5  30015  2pthdlem1  30016  s3wwlks2on  30042  sps3wwlks2on  30043  wpthswwlks2on  30050  elwspths2spth  30056  rusgrnumwwlks  30063  umgrclwwlkge2  30079  clwlkclwwlklem2a4  30085  clwlkclwwlk  30090  clwlkclwwlkflem  30092  clwwisshclwws  30103  isclwwlknx  30124  clwwlknwwlksnb  30143  eclclwwlkn1  30163  clwwlknonel  30183  clwwlknun  30200  3wlkdlem6  30253  frgrncvvdeqlem9  30395  fusgreg2wsp  30424  numclwwlk2lem1lem  30430  extwwlkfab  30440  frgrreggt1  30481  ubthlem1  30959  norm-i  31218  hoeq  31849  nmopgt0  32001  pjimai  32265  chirredi  32483  addltmulALT  32535  opreu2reuALT  32564  sbcies  32575  rmounid  32582  iunrdx  32651  disjrdx  32679  sgnneg  32924  sgn3da  32925  archiabl  33277  islbs5  33458  ist0cld  33996  oms0  34460  eulerpartgbij  34535  reprinrn  34781  usgrgt2cycl  35331  satfv1lem  35563  satf0op  35578  dmopab3rexdif  35606  satefvfmla0  35619  mrsubrn  35714  topfne  36555  unbdqndv1  36787  bj-hbntbi  37020  bj-issetwt  37201  bj-clel3gALT  37374  copsex2d  37472  bj-elid6  37503  dfgcd3  37657  topdifinfeq  37683  wl-sbalnae  37904  sin2h  37948  poimirlem16  37974  poimirlem17  37975  poimirlem25  37983  mbfresfi  38004  itg2addnclem  38009  itg2addnclem2  38010  itg2addnclem3  38011  ftc1anclem1  38031  isidlc  38353  eldmressnALTV  38617  islshpsm  39443  lshpkrlem1  39573  opcon1b  39661  lautlt  40554  lauteq  40558  idlaut  40559  diblsmopel  41634  doch11  41836  recbothd  42448  aks4d1p8d2  42541  aks4d1p8  42543  isprimroot2  42550  posbezout  42556  aks6d1c5lem1  42592  sticksstones1  42602  sticksstones11  42612  sticksstones22  42624  aks6d1c6lem3  42628  aks6d1c6lem4  42629  aks6d1c7  42640  aks5lem8  42657  f1o2d2  42691  dvdsexpnn0  42783  redvmptabs  42809  redivne0bd  42899  prjsprellsp  43061  prjspeclsp  43062  abbibw  43127  istopclsd  43149  eqrabdioph  43226  rexzrexnn0  43253  zindbi  43395  expdiophlem2  43471  onsupeqmax  43695  onsupeqnmax  43696  ordeldif  43707  infordmin  43980  inintabd  44027  cnvcnvintabd  44048  cnvintabd  44051  sqrtcvallem1  44079  reabsifneg  44080  fsovrfovd  44457  ntrclsiso  44515  ntrneifv3  44530  ntrneineine0lem  44531  ntrneicls11  44538  suprleubrd  44614  suprlubrd  44616  lemuldiv4d  44619  pm14.122a  44870  3impexpbicomi  44929  onfrALTlem5  44990  bitr3VD  45296  onfrALTlem5VD  45332  csbrngVD  45343  pwpwuni  45509  supxrre3  45776  xrralrecnnge  45840  eliooshift  45957  limsupre2lem  46173  liminflimsupclim  46256  xlimbr  46276  smfrec  47238  fsetprcnexALT  47525  f1cof1b  47540  reuf1odnf  47570  2reuimp  47578  ralbinrald  47585  afvco2  47639  dfatdmfcoafv2  47717  recnmulnred  47768  sqrtnegnre  47770  subsubelfzo0  47790  ceilbi  47800  ichcircshi  47929  sprvalpwle2  47964  sprsymrelf1lem  47966  sbcpr  47996  poprelb  47999  31prm  48075  requad01  48112  dfeven3  48149  iseven5  48155  0noddALTV  48180  2noddALTV  48184  fpprmod  48218  sbgoldbaltlem1  48270  bgoldbtbndlem2  48297  dfclnbgr2  48314  dfsclnbgr2  48337  dfvopnbgr2  48344  dfsclnbgr6  48349  isuspgrim0lem  48384  usgrgrtrirex  48441  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgn4cyclex  48617  0nodd  48661  2nodd  48663  isassintop  48701  uzlidlring  48726  funcringcsetcALTV2lem8  48788  funcringcsetclem8ALTV  48811  nn0sumltlt  48841  ply1mulgsumlem2  48878  islindeps  48944  lindslinindsimp1  48948  lindslinindsimp2  48954  snlindsntor  48962  zlmodzxznm  48988  ldepslinc  49000  elbigo2  49043  elbigolo1  49048  logblt1b  49055  fldivexpfllog2  49056  nnolog2flm1  49081  digexp  49098  nn0sumshdiglemB  49111  itsclquadeu  49268  itscnhlinecirc02p  49276  ipolublem  49476  ipoglblem  49479