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  267  bitr2d  279  bitr3d  280  bitr4d  281  bitr2id  283  bitr2di  287  con1bid  354  pm5.5  360  imnot  364  baibr  535  rbaib  537  baibd  538  anabs5  661  annotanannot  833  pm5.55  946  pm5.54  1015  ninba  1019  pm5.75  1026  sbequ12r  2243  sbal1  2525  euor2  2605  eqabcdv  2864  necon3bbid  2971  necon4bbid  2975  ralanid  3088  rexanid  3089  sbralieALT  3352  ralcom2  3370  rmoanid  3383  reuanid  3384  rabrabi  3447  gencbvex  3537  sbhypfOLD  3541  alexeqg  3648  clel2g  3656  clel2gOLD  3657  clel3g  3659  clel4g  3661  reurab  3706  reu8  3738  sbceq2a  3799  sbcco2  3814  reu8nf  3881  notabw  4313  2reu4lem  4531  reurexprg  4714  raltpd  4791  ssdifsn  4798  uniprg  4932  disjxun  5152  opabidw  5532  opabid  5533  soeq2  5618  sotrine  5634  posn  5769  xpiindi  5844  dmopab2rex  5926  elpredg  6329  fvopab6  7045  cbvfo  7305  f1eqcocnv  7317  isoid  7344  isoini  7353  isosolem  7362  riotaeqimp  7410  riotarab  7426  resoprab2  7547  tfisi  7874  tfinds2  7879  f1oweALT  7991  dfoprab3  8073  opiota  8078  xpord2indlem  8166  xpord3inddlem  8173  mpocurryd  8288  oalimcl  8594  omword  8604  oeword  8624  nnacan  8662  nnmcan  8668  mapsnd  8919  findcard2s  9206  funisfsupp  9412  suppeqfsuppbi  9423  eqinf  9528  inflb  9533  infglb  9534  infglbb  9535  infltoreq  9546  infempty  9551  brwdomn0  9613  cantnfp1lem3  9724  ssrankr1  9879  r1pw  9889  djulf1o  9956  djurf1o  9957  aleph11  10128  alephval3  10154  gch-kn  10721  wunex2  10782  lttri2  11347  wloglei  11797  divne0b  11935  lemul1  12121  nnnle0  12301  div4p1lem1div2  12523  nn0ind-raph  12718  zindd  12719  suprfinzcl  12732  rebtwnz  12987  qreccl  13009  elpq  13015  xrlttri2  13179  2resupmax  13225  xmulneg1  13306  iooshf  13461  difreicc  13519  fzofzim  13737  elfzomelpfzo  13795  elfznelfzo  13796  zmodid2  13924  2submod  13957  modfzo0difsn  13968  om2uzlti  13975  expcan  14193  hashvnfin  14383  hashneq0  14387  prhash2ex  14422  hashgt0elex  14424  hashgt12el  14445  hashgt12el2  14446  hashbclem  14475  hashf1lem2  14479  prprrab  14496  swrd0  14679  pfxn0  14707  swrdswrd  14726  pfxccat3  14755  repswswrd  14805  cshf1  14831  cshw1repsw  14844  relexpindlem  15081  absz  15329  iserex  15674  prodrb  15947  absdvdsb  16290  dvdsabsb  16291  modmulconst  16303  dvdsadd  16317  dvdsabseq  16328  mod2eq0even  16361  oddnn02np1  16363  oddge22np1  16364  evennn02n  16365  evennn2n  16366  zeo5  16371  sadadd2lem2  16463  smupvallem  16496  gcdass  16561  lcmdvds  16622  lcmass  16628  divgcdcoprm0  16679  divgcdcoprmex  16680  1nprm  16693  dvdsnprmd  16704  prmdvdssq  16732  ncoprmlnprm  16743  isevengcd2  16745  m1dvdsndvds  16813  cshws0  17117  sbcie3s  17177  dfiso2  17801  initoid  18036  termoid  18037  funcestrcsetclem8  18184  lublecllem  18398  odudlatb  18563  sgrppropd  18737  issubm2  18807  mgm2nsgrplem2  18922  nsgacs  19170  cycsubg2  19218  gapm  19314  sscntz  19334  pgrpsubgsymgbi  19418  f1omvdcnv  19454  pmtrprfvalrn  19498  odval2  19561  lsmcntz  19689  rngpropd  20169  rnghmf1o  20446  isrngim2  20447  rhmf1o  20485  isrim  20486  isrimOLD  20487  dfprm2  21475  pzriprnglem10  21492  psgnfix2  21608  islinds3  21845  islindf4  21849  snifpsrbag  21930  gsumply1eq  22300  mdetdiaglem  22591  mdetunilem9  22613  slesolinv  22673  slesolex  22675  cpmatel2  22706  m2cpmghm  22737  m2cpminvid2  22748  pm2mpf1  22792  chfacfscmul0  22851  chfacfscmulfsupp  22852  chfacfpmmul0  22855  chfacfpmmulfsupp  22856  isopn2  23027  cmpsub  23395  connsub  23416  ncvs1  25176  rrxmvallem  25423  itg1mulc  25725  lhop1  26038  mdegleb  26088  lawcos  26841  leibpi  26967  2lgslem1a  27417  2sq2  27459  sletric  27791  0reno  28390  colinearalg  28886  edg0iedg0  29033  uhgreq12g  29043  uhgrvtxedgiedgb  29114  usgredg2v  29205  edg0usgr  29231  dfnbgr2  29315  nbuhgr  29321  nbusgredgeu0  29346  nb3grprlem1  29358  nb3grpr  29360  uvtx2vtx1edgb  29377  redwlk  29651  uhgrwkspthlem2  29733  usgr2wlkspth  29738  pthdlem1  29745  cyclnspth  29779  crctcshwlkn0lem1  29786  crctcshwlkn0lem4  29789  crctcsh  29800  iswwlksnx  29816  wwlksm1edg  29857  wwlksnextsurj  29876  wwlksnextproplem3  29887  2wlkdlem4  29904  2wlkdlem5  29905  2pthdlem1  29906  s3wwlks2on  29932  wpthswwlks2on  29937  elwspths2spth  29943  rusgrnumwwlks  29950  umgrclwwlkge2  29966  clwlkclwwlklem2a4  29972  clwlkclwwlk  29977  clwlkclwwlkflem  29979  clwwisshclwws  29990  isclwwlknx  30011  clwwlknwwlksnb  30030  eclclwwlkn1  30050  clwwlknonel  30070  clwwlknun  30087  3wlkdlem6  30140  frgrncvvdeqlem9  30282  fusgreg2wsp  30311  numclwwlk2lem1lem  30317  extwwlkfab  30327  frgrreggt1  30368  ubthlem1  30845  norm-i  31104  hoeq  31735  nmopgt0  31887  pjimai  32151  chirredi  32369  addltmulALT  32421  bian1d  32427  opreu2reuALT  32448  sbcies  32459  rmounid  32466  iunrdx  32530  disjrdx  32557  cnvoprabOLD  32679  archiabl  33123  islbs5  33318  ist0cld  33724  oms0  34207  eulerpartgbij  34282  sgnneg  34450  sgn3da  34451  reprinrn  34540  usgrgt2cycl  35043  satfv1lem  35275  satf0op  35290  dmopab3rexdif  35318  satefvfmla0  35331  mrsubrn  35426  topfne  36152  unbdqndv1  36297  bj-hbntbi  36495  bj-issetwt  36666  bj-clel3gALT  36840  copsex2d  36931  bj-elid6  36962  dfgcd3  37116  topdifinfeq  37142  wl-sbalnae  37342  sin2h  37396  poimirlem16  37422  poimirlem17  37423  poimirlem25  37431  mbfresfi  37452  itg2addnclem  37457  itg2addnclem2  37458  itg2addnclem3  37459  ftc1anclem1  37479  isidlc  37801  eldmressnALTV  38055  islshpsm  38763  lshpkrlem1  38893  opcon1b  38981  lautlt  39875  lauteq  39879  idlaut  39880  diblsmopel  40955  doch11  41157  recbothd  41776  aks4d1p8d2  41869  aks4d1p8  41871  isprimroot2  41878  posbezout  41884  aks6d1c5lem1  41920  sticksstones1  41930  sticksstones11  41940  sticksstones22  41952  aks6d1c6lem3  41956  aks6d1c6lem4  41957  aks6d1c7  41968  aks5lem8  41985  metakunt16  42003  f1o2d2  42054  dvdsexpnn0  42135  prjsprellsp  42376  prjspeclsp  42377  abbibw  42445  istopclsd  42469  eqrabdioph  42546  rexzrexnn0  42573  zindbi  42716  expdiophlem2  42792  onsupeqmax  43023  onsupeqnmax  43024  ordeldif  43036  infordmin  43311  inintabd  43358  cnvcnvintabd  43379  cnvintabd  43382  sqrtcvallem1  43410  reabsifneg  43411  fsovrfovd  43788  ntrclsiso  43846  ntrneifv3  43861  ntrneineine0lem  43862  ntrneicls11  43869  suprleubrd  43945  suprlubrd  43947  lemuldiv4d  43950  pm14.122a  44208  3impexpbicomi  44268  onfrALTlem5  44330  bitr3VD  44637  onfrALTlem5VD  44673  csbrngVD  44684  pwpwuni  44770  supxrre3  45051  xrralrecnnge  45116  eliooshift  45235  limsupre2lem  45456  liminflimsupclim  45539  xlimbr  45559  smfrec  46521  fsetprcnexALT  46788  f1cof1b  46801  reuf1odnf  46831  2reuimp  46839  ralbinrald  46846  afvco2  46900  dfatdmfcoafv2  46978  recnmulnred  47029  sqrtnegnre  47031  subsubelfzo0  47050  ichcircshi  47137  sprvalpwle2  47172  sprsymrelf1lem  47174  sbcpr  47204  poprelb  47207  31prm  47280  requad01  47304  dfeven3  47341  iseven5  47347  0noddALTV  47372  2noddALTV  47376  fpprmod  47410  sbgoldbaltlem1  47462  bgoldbtbndlem2  47489  dfclnbgr2  47506  dfsclnbgr2  47524  dfvopnbgr2  47531  dfsclnbgr6  47536  isuspgrim0lem  47561  0nodd  47669  2nodd  47671  isassintop  47709  uzlidlring  47734  funcringcsetcALTV2lem8  47796  funcringcsetclem8ALTV  47819  nn0sumltlt  47851  ply1mulgsumlem2  47892  islindeps  47958  lindslinindsimp1  47962  lindslinindsimp2  47968  snlindsntor  47976  zlmodzxznm  48002  ldepslinc  48014  difmodm1lt  48032  elbigo2  48062  elbigolo1  48067  logblt1b  48074  fldivexpfllog2  48075  nnolog2flm1  48100  digexp  48117  nn0sumshdiglemB  48130  itsclquadeu  48287  itscnhlinecirc02p  48295  ipolublem  48434  ipoglblem  48437