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  834  pm5.55  950  pm5.54  1019  ninba  1023  pm5.75  1030  sbequ12r  2251  sbal1  2532  euor2  2612  eqabcdv  2875  necon3bbid  2977  necon4bbid  2981  ralanid  3094  rexanid  3095  sbralieALT  3358  ralcom2  3376  rmoanid  3389  reuanid  3390  rabrabi  3455  gencbvex  3540  sbhypfOLD  3544  alexeqg  3650  clel2g  3658  clel3g  3660  clel4g  3662  reurab  3706  reu8  3738  sbceq2a  3799  sbcco2  3814  reu8nf  3876  notabw  4312  2reu4lem  4521  reurexprg  4703  raltpd  4780  ssdifsn  4787  uniprg  4922  disjxun  5140  opabidw  5528  opabid  5529  soeq2  5613  sotrine  5631  posn  5770  xpiindi  5845  dmopab2rex  5927  elpredg  6334  fvopab6  7049  cbvfo  7310  f1eqcocnv  7322  isoid  7350  isoini  7359  isosolem  7368  riotaeqimp  7415  riotarab  7431  resoprab2  7553  tfisi  7881  tfinds2  7886  f1oweALT  7998  dfoprab3  8080  opiota  8085  xpord2indlem  8173  xpord3inddlem  8180  mpocurryd  8295  oalimcl  8599  omword  8609  oeword  8629  nnacan  8667  nnmcan  8673  mapsnd  8927  findcard2s  9206  funisfsupp  9408  suppeqfsuppbi  9420  eqinf  9525  inflb  9530  infglb  9531  infglbb  9532  infltoreq  9543  infempty  9548  brwdomn0  9610  cantnfp1lem3  9721  ssrankr1  9876  r1pw  9886  djulf1o  9953  djurf1o  9954  aleph11  10125  alephval3  10151  gch-kn  10718  wunex2  10779  lttri2  11344  wloglei  11796  divne0b  11934  lemul1  12120  nnnle0  12300  div4p1lem1div2  12523  nn0ind-raph  12720  zindd  12721  suprfinzcl  12734  rebtwnz  12990  qreccl  13012  elpq  13018  xrlttri2  13185  2resupmax  13231  xmulneg1  13312  iooshf  13467  difreicc  13525  fzofzim  13750  elfzomelpfzo  13811  elfznelfzo  13812  zmodid2  13940  2submod  13974  modfzo0difsn  13985  om2uzlti  13992  expcan  14210  hashvnfin  14400  hashneq0  14404  prhash2ex  14439  hashgt0elex  14441  hashgt12el  14462  hashgt12el2  14463  hashbclem  14492  hashf1lem2  14496  prprrab  14513  swrd0  14697  pfxn0  14725  swrdswrd  14744  pfxccat3  14773  repswswrd  14823  cshf1  14849  cshw1repsw  14862  relexpindlem  15103  absz  15351  iserex  15694  prodrb  15969  absdvdsb  16313  dvdsabsb  16314  modmulconst  16326  dvdsadd  16340  dvdsabseq  16351  mod2eq0even  16384  oddnn02np1  16386  oddge22np1  16387  evennn02n  16388  evennn2n  16389  zeo5  16394  sadadd2lem2  16488  smupvallem  16521  gcdass  16585  lcmdvds  16646  lcmass  16652  divgcdcoprm0  16703  divgcdcoprmex  16704  1nprm  16717  dvdsnprmd  16728  prmdvdssq  16756  ncoprmlnprm  16766  isevengcd2  16768  m1dvdsndvds  16837  cshws0  17140  sbcie3s  17200  dfiso2  17817  initoid  18047  termoid  18048  funcestrcsetclem8  18193  lublecllem  18406  odudlatb  18571  sgrppropd  18745  issubm2  18818  mgm2nsgrplem2  18933  nsgacs  19181  cycsubg2  19229  gapm  19325  sscntz  19345  pgrpsubgsymgbi  19427  f1omvdcnv  19463  pmtrprfvalrn  19507  odval2  19570  lsmcntz  19698  rngpropd  20172  rnghmf1o  20453  isrngim2  20454  rhmf1o  20492  isrim  20493  isrimOLD  20494  dfprm2  21485  pzriprnglem10  21502  psgnfix2  21618  islinds3  21855  islindf4  21859  snifpsrbag  21941  gsumply1eq  22314  mdetdiaglem  22605  mdetunilem9  22627  slesolinv  22687  slesolex  22689  cpmatel2  22720  m2cpmghm  22751  m2cpminvid2  22762  pm2mpf1  22806  chfacfscmul0  22865  chfacfscmulfsupp  22866  chfacfpmmul0  22869  chfacfpmmulfsupp  22870  isopn2  23041  cmpsub  23409  connsub  23430  ncvs1  25192  rrxmvallem  25439  itg1mulc  25740  lhop1  26054  mdegleb  26104  lawcos  26860  leibpi  26986  2lgslem1a  27436  2sq2  27478  sletric  27810  0reno  28430  colinearalg  28926  edg0iedg0  29073  uhgreq12g  29083  uhgrvtxedgiedgb  29154  usgredg2v  29245  edg0usgr  29271  dfnbgr2  29355  nbuhgr  29361  nbusgredgeu0  29386  nb3grprlem1  29398  nb3grpr  29400  uvtx2vtx1edgb  29417  redwlk  29691  uhgrwkspthlem2  29775  usgr2wlkspth  29780  pthdlem1  29787  cyclnspth  29822  crctcshwlkn0lem1  29831  crctcshwlkn0lem4  29834  crctcsh  29845  iswwlksnx  29861  wwlksm1edg  29902  wwlksnextsurj  29921  wwlksnextproplem3  29932  2wlkdlem4  29949  2wlkdlem5  29950  2pthdlem1  29951  s3wwlks2on  29977  wpthswwlks2on  29982  elwspths2spth  29988  rusgrnumwwlks  29995  umgrclwwlkge2  30011  clwlkclwwlklem2a4  30017  clwlkclwwlk  30022  clwlkclwwlkflem  30024  clwwisshclwws  30035  isclwwlknx  30056  clwwlknwwlksnb  30075  eclclwwlkn1  30095  clwwlknonel  30115  clwwlknun  30132  3wlkdlem6  30185  frgrncvvdeqlem9  30327  fusgreg2wsp  30356  numclwwlk2lem1lem  30362  extwwlkfab  30372  frgrreggt1  30413  ubthlem1  30890  norm-i  31149  hoeq  31780  nmopgt0  31932  pjimai  32196  chirredi  32414  addltmulALT  32466  bian1d  32476  opreu2reuALT  32497  sbcies  32508  rmounid  32515  iunrdx  32577  disjrdx  32605  archiabl  33206  islbs5  33409  ist0cld  33833  oms0  34300  eulerpartgbij  34375  sgnneg  34544  sgn3da  34545  reprinrn  34634  usgrgt2cycl  35136  satfv1lem  35368  satf0op  35383  dmopab3rexdif  35411  satefvfmla0  35424  mrsubrn  35519  topfne  36356  unbdqndv1  36510  bj-hbntbi  36706  bj-issetwt  36877  bj-clel3gALT  37050  copsex2d  37141  bj-elid6  37172  dfgcd3  37326  topdifinfeq  37352  wl-sbalnae  37564  sin2h  37618  poimirlem16  37644  poimirlem17  37645  poimirlem25  37653  mbfresfi  37674  itg2addnclem  37679  itg2addnclem2  37680  itg2addnclem3  37681  ftc1anclem1  37701  isidlc  38023  eldmressnALTV  38274  islshpsm  38982  lshpkrlem1  39112  opcon1b  39200  lautlt  40094  lauteq  40098  idlaut  40099  diblsmopel  41174  doch11  41376  recbothd  41994  aks4d1p8d2  42087  aks4d1p8  42089  isprimroot2  42096  posbezout  42102  aks6d1c5lem1  42138  sticksstones1  42148  sticksstones11  42158  sticksstones22  42170  aks6d1c6lem3  42174  aks6d1c6lem4  42175  aks6d1c7  42186  aks5lem8  42203  metakunt16  42222  f1o2d2  42274  dvdsexpnn0  42374  redvmptabs  42395  prjsprellsp  42626  prjspeclsp  42627  abbibw  42692  istopclsd  42716  eqrabdioph  42793  rexzrexnn0  42820  zindbi  42963  expdiophlem2  43039  onsupeqmax  43263  onsupeqnmax  43264  ordeldif  43276  infordmin  43550  inintabd  43597  cnvcnvintabd  43618  cnvintabd  43621  sqrtcvallem1  43649  reabsifneg  43650  fsovrfovd  44027  ntrclsiso  44085  ntrneifv3  44100  ntrneineine0lem  44101  ntrneicls11  44108  suprleubrd  44184  suprlubrd  44186  lemuldiv4d  44189  pm14.122a  44446  3impexpbicomi  44506  onfrALTlem5  44567  bitr3VD  44874  onfrALTlem5VD  44910  csbrngVD  44921  pwpwuni  45067  supxrre3  45341  xrralrecnnge  45406  eliooshift  45524  limsupre2lem  45744  liminflimsupclim  45827  xlimbr  45847  smfrec  46809  fsetprcnexALT  47079  f1cof1b  47094  reuf1odnf  47124  2reuimp  47132  ralbinrald  47139  afvco2  47193  dfatdmfcoafv2  47271  recnmulnred  47322  sqrtnegnre  47324  subsubelfzo0  47343  ichcircshi  47446  sprvalpwle2  47481  sprsymrelf1lem  47483  sbcpr  47513  poprelb  47516  31prm  47589  requad01  47613  dfeven3  47650  iseven5  47656  0noddALTV  47681  2noddALTV  47685  fpprmod  47719  sbgoldbaltlem1  47771  bgoldbtbndlem2  47798  dfclnbgr2  47815  dfsclnbgr2  47837  dfvopnbgr2  47844  dfsclnbgr6  47849  isuspgrim0lem  47876  usgrgrtrirex  47922  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  0nodd  48091  2nodd  48093  isassintop  48131  uzlidlring  48156  funcringcsetcALTV2lem8  48218  funcringcsetclem8ALTV  48241  nn0sumltlt  48271  ply1mulgsumlem2  48309  islindeps  48375  lindslinindsimp1  48379  lindslinindsimp2  48385  snlindsntor  48393  zlmodzxznm  48419  ldepslinc  48431  difmodm1lt  48448  elbigo2  48478  elbigolo1  48483  logblt1b  48490  fldivexpfllog2  48491  nnolog2flm1  48516  digexp  48533  nn0sumshdiglemB  48546  itsclquadeu  48703  itscnhlinecirc02p  48711  ipolublem  48890  ipoglblem  48893