Theorem bicomd 226

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 225	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 221	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  impbid2  229  imbitrrid  249  ibir  271  bitr2d  283  bitr3d  284  bitr4d  285  bitr2id  287  bitr2di  291  con1bid  358  pm5.5  364  imnot  368  baibr  546  rbaib  548  baibd  549  anabs5  676  annotanannot  848  pm5.55  963  pm5.54  1035  ninba  1039  pm5.75  1046  sbequ12r  2290  sbal1  2560  euor2  2641  eqabcdv  2897  necon3bbid  2995  necon4bbid  2999  ralanid  3113  rexanid  3114  sbralieALT  3342  ralcom2  3365  rmoanid  3378  reuanid  3379  rabrabi  3433  gencbvex  3509  alexeqg  3607  clel2g  3615  clel3g  3617  clel4g  3619  reurab  3661  reu8  3693  sbceq2a  3753  sbcco2  3768  reu8nf  3827  notabw  4260  2reu4lem  4481  reurexprg  4664  raltpd  4741  ssdifsn  4750  uniprg  4885  disjxun  5103  opabidw  5501  opabid  5502  soeq2  5584  sotrine  5602  posn  5741  xpiindi  5816  dmopab2rex  5903  elpredg  6324  fvopab6  7036  cbvfo  7304  f1eqcocnv  7316  isoid  7344  isoini  7353  isosolem  7362  riotaeqimp  7410  riotarab  7426  resoprab2  7546  tfisi  7877  tfinds2  7882  f1oweALT  7991  dfoprab3  8073  opiota  8078  mpof1o2d  8147  xpord2indlem  8174  xpord3inddlem  8181  mpocurryd  8297  oalimcl  8579  omword  8589  oeword  8610  nnacan  8648  nnmcan  8654  mapsnd  8925  findcard2s  9192  funisfsupp  9370  suppeqfsuppbi  9381  eqinf  9487  inflb  9492  infglb  9493  infglbb  9494  infltoreq  9506  infempty  9511  brwdomn0  9573  cantnfp1lem3  9691  ssrankr1  9857  r1pw  9869  djulf1o  10003  djurf1o  10004  aleph11  10173  alephval3  10199  gch-kn  10772  wunex2  10833  lttri2  11402  wloglei  11858  divne0b  11995  lemul1  12179  nnnle0  12381  div4p1lem1div2  12611  nn0ind-raph  12809  zindd  12810  suprfinzcl  12823  rebtwnz  13084  qreccl  13107  elpq  13113  xrlttri2  13281  2resupmax  13328  xmulneg1  13409  iooshf  13567  difreicc  13625  fzofzim  13854  elfzomelpfzo  13917  elfznelfzo  13918  zmodid2  14049  2submod  14085  modfzo0difsn  14096  om2uzlti  14103  expcan  14322  hashvnfin  14514  hashneq0  14518  prhash2ex  14553  hashgt0elex  14555  hashgt12el  14577  hashgt12el2  14578  hashbclem  14607  hashf1lem2  14611  prprrab  14628  swrd0  14819  pfxn0  14847  swrdswrd  14865  pfxccat3  14894  repswswrd  14946  cshf1  14972  cshw1repsw  14985  relexpindlem  15228  sgnneg  15265  sgn3da  15266  absz  15490  iserex  15836  prodrb  16111  absdvdsb  16456  dvdsabsb  16457  modmulconst  16470  dvdsadd  16484  dvdsabseq  16495  mod2eq0even  16528  oddnn02np1  16530  oddge22np1  16531  evennn02n  16532  evennn2n  16533  zeo5  16538  sadadd2lem2  16632  smupvallem  16665  gcdass  16732  lcmdvds  16795  lcmass  16801  divgcdcoprm0  16852  divgcdcoprmex  16853  1nprm  16866  dvdsnprmd  16877  prmdvdssq  16906  ncoprmlnprm  16916  isevengcd2  16918  m1dvdsndvds  16988  cshws0  17291  sbcie3s  17352  dfiso2  17959  initoid  18188  termoid  18189  funcestrcsetclem8  18333  lublecllem  18544  odudlatb  18711  sgrppropd  18932  issubm2  19011  mgm2nsgrplem2  19130  nsgacs  19384  cycsubg2  19437  gapm  19532  sscntz  19552  pgrpsubgsymgbi  19634  f1omvdcnv  19670  pmtrprfvalrn  19714  odval2  19777  lsmcntz  19905  rngpropd  20408  rnghmf1o  20694  isrngim2  20695  rhmf1o  20739  isrim  20740  df2idl2crng  21589  dfprm2  21791  pzriprnglem10  21808  psgnfix2  21917  islinds3  22152  islindf4  22156  snifpsrbag  22240  gsumply1eq  22639  mdetdiaglem  22925  mdetunilem9  22947  slesolinv  23010  slesolex  23012  cpmatel2  23043  m2cpmghm  23074  m2cpminvid2  23085  pm2mpf1  23129  chfacfscmul0  23188  chfacfscmulfsupp  23189  chfacfpmmul0  23192  chfacfpmmulfsupp  23193  isopn2  23362  cmpsub  23730  connsub  23751  ncvs1  25490  rrxmvallem  25737  itg1mulc  26037  lhop1  26346  mdegleb  26394  lawcos  27156  leibpi  27282  2lgslem1a  27730  2sq2  27772  lestric  28137  bdayons  28674  n0subs2  28762  bdaypw2n0bndlem  28861  angmgmaddov2  29401  colinearalg  29500  edg0iedg0  29645  uhgreq12g  29655  uhgrvtxedgiedgb  29726  usgredg2v  29820  edg0usgr  29846  dfnbgr2  29930  nbuhgr  29936  nbusgredgeu0  29961  nb3grprlem1  29973  nb3grpr  29975  uvtx2vtx1edgb  29992  redwlk  30263  uhgrwkspthlem2  30352  usgr2wlkspth  30357  pthdlem1  30364  cyclnspth  30401  crctcshwlkn0lem1  30411  crctcshwlkn0lem4  30414  crctcsh  30425  iswwlksnx  30441  wwlksm1edg  30482  wwlksnextsurj  30501  wwlksnextproplem3  30512  2wlkdlem4  30529  2wlkdlem5  30530  2pthdlem1  30531  s3wwlks2on  30557  sps3wwlks2on  30558  wpthswwlks2on  30565  elwspths2spth  30571  rusgrnumwwlks  30578  umgrclwwlkge2  30594  clwlkclwwlklem2a4  30600  clwlkclwwlk  30605  clwlkclwwlkflem  30607  clwwisshclwws  30618  isclwwlknx  30639  clwwlknwwlksnb  30658  eclclwwlkn1  30678  clwwlknonel  30698  clwwlknun  30715  3wlkdlem6  30778  frgrncvvdeqlem9  30920  fusgreg2wsp  30949  numclwwlk2lem1lem  30955  extwwlkfab  30965  frgrreggt1  31006  ubthlem1  31484  norm-i  31743  hoeq  32374  nmopgt0  32526  pjimai  32790  chirredi  33008  addltmulALT  33102  opreu2reuALT  33127  sbcies  33138  rmounid  33145  iunrdx  33212  disjrdx  33239  archiabl  33812  islbs5  33988  ist0cld  34518  oms0  34982  eulerpartgbij  35057  reprinrn  35300  usgrgt2cycl  36020  satfv1lem  36248  satf0op  36263  dmopab3rexdif  36291  satefvfmla0  36304  mrsubrn  36399  topfne  37269  unbdqndv1  37501  bj-hbntbi  37733  bj-issetwt  37914  bj-clel3gALT  38102  copsex2d  38200  bj-elid6  38231  dfgcd3  38385  topdifinfeq  38413  wl-sbalnae  38634  sin2h  38673  poimirlem16  38694  poimirlem17  38695  poimirlem25  38703  mbfresfi  38724  itg2addnclem  38729  itg2addnclem2  38730  itg2addnclem3  38731  ftc1anclem1  38751  findcard4  38772  isidlc  39089  eldmressnALTV  39351  islshpsm  40177  lshpkrlem1  40307  opcon1b  40395  lautlt  41288  lauteq  41292  idlaut  41293  diblsmopel  42368  doch11  42570  recbothd  43182  aks4d1p8d2  43275  aks4d1p8  43277  isprimroot2  43284  posbezout  43290  aks6d1c5lem1  43326  sticksstones1  43336  sticksstones11  43346  sticksstones22  43358  aks6d1c6lem3  43362  aks6d1c6lem4  43363  aks6d1c7  43374  aks5lem8  43391  dvdsexpnn0  43526  redvmptabs  43551  redivne0bd  43641  prjsprellsp  43779  prjspeclsp  43780  abbibw  43828  istopclsd  43851  eqrabdioph  43928  rexzrexnn0  43951  zindbi  44093  expdiophlem2  44169  onsupeqmax  44388  onsupeqnmax  44389  ordeldif  44400  infordmin  44673  inintabd  44720  cnvcnvintabd  44740  cnvintabd  44743  sqrtcvallem1  44771  reabsifneg  44772  fsovrfovd  45149  ntrclsiso  45207  ntrneifv3  45222  ntrneineine0lem  45223  ntrneicls11  45230  suprleubrd  45306  suprlubrd  45308  lemuldiv4d  45311  pm14.122a  45545  3impexpbicomi  45603  onfrALTlem5  45664  bitr3VD  45970  onfrALTlem5VD  46006  csbrngVD  46017  pwpwuni  46213  supxrre3  46476  xrralrecnnge  46540  eliooshift  46657  limsupre2lem  46873  liminflimsupclim  46956  xlimbr  46976  smfrec  47938  fsetprcnexALT  48271  f1cof1b  48286  reuf1odnf  48317  2reuimp  48325  ralbinrald  48332  afvco2  48385  dfatdmfcoafv2  48463  recnmulnred  48514  sqrtnegnre  48516  subsubelfzo0  48536  ceilbi  48546  ichcircshi  48675  sprvalpwle2  48710  sprsymrelf1lem  48712  sbcpr  48742  poprelb  48745  31prm  48821  requad01  48858  dfeven3  48895  iseven5  48901  0noddALTV  48926  2noddALTV  48930  fpprmod  48964  sbgoldbaltlem1  49016  bgoldbtbndlem2  49043  dfclnbgr2  49060  dfsclnbgr2  49083  dfvopnbgr2  49090  dfsclnbgr6  49095  isuspgrim0lem  49130  usgrgrtrirex  49187  usgrexmpl2nb1  49269  usgrexmpl2nb2  49270  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  pgnbgreunbgrlem2lem3  49353  pgn4cyclex  49363  0nodd  49406  2nodd  49408  isassintop  49446  uzlidlring  49471  funcringcsetcALTV2lem8  49533  funcringcsetclem8ALTV  49556  prmringnzring  49573  dfidom2  49579  idomcanl  49583  nn0sumltlt  49601  ply1mulgsumlem2  49638  islindeps  49704  lindslinindsimp1  49708  lindslinindsimp2  49714  snlindsntor  49722  zlmodzxznm  49748  ldepslinc  49760  elbigo2  49803  elbigolo1  49808  logblt1b  49815  fldivexpfllog2  49816  nnolog2flm1  49841  digexp  49858  nn0sumshdiglemB  49871  itsclquadeu  50028  itscnhlinecirc02p  50036  ipolublem  50239  ipoglblem  50242  dvsec  51070  dvcsc  51071  dvcot  51072  ralrals  51118  rexrals  51119  ralals  51124  rexals  51125