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  2287  sbal1  2557  euor2  2638  eqabcdv  2894  necon3bbid  2992  necon4bbid  2996  ralanid  3110  rexanid  3111  sbralieALT  3339  ralcom2  3362  rmoanid  3375  reuanid  3376  rabrabi  3430  gencbvex  3506  alexeqg  3605  clel2g  3613  clel3g  3615  clel4g  3617  reurab  3659  reu8  3691  sbceq2a  3751  sbcco2  3766  reu8nf  3824  notabw  4259  2reu4lem  4479  reurexprg  4665  raltpd  4742  ssdifsn  4751  uniprg  4883  disjxun  5101  opabidw  5502  opabid  5503  soeq2  5585  sotrine  5603  posn  5741  xpiindi  5815  dmopab2rex  5901  elpredg  6313  fvopab6  7021  cbvfo  7290  f1eqcocnv  7302  isoid  7330  isoini  7339  isosolem  7348  riotaeqimp  7396  riotarab  7412  resoprab2  7532  tfisi  7855  tfinds2  7860  f1oweALT  7969  dfoprab3  8051  opiota  8056  mpof1o2d  8123  xpord2indlem  8145  xpord3inddlem  8152  mpocurryd  8267  oalimcl  8547  omword  8557  oeword  8578  nnacan  8616  nnmcan  8622  mapsnd  8893  findcard2s  9160  funisfsupp  9337  suppeqfsuppbi  9349  eqinf  9455  inflb  9460  infglb  9461  infglbb  9462  infltoreq  9474  infempty  9479  brwdomn0  9541  cantnfp1lem3  9659  ssrankr1  9817  r1pw  9827  djulf1o  9917  djurf1o  9918  aleph11  10087  alephval3  10113  gch-kn  10686  wunex2  10747  lttri2  11316  wloglei  11770  divne0b  11907  lemul1  12091  nnnle0  12293  div4p1lem1div2  12523  nn0ind-raph  12721  zindd  12722  suprfinzcl  12735  rebtwnz  12996  qreccl  13019  elpq  13025  xrlttri2  13193  2resupmax  13240  xmulneg1  13321  iooshf  13479  difreicc  13537  fzofzim  13765  elfzomelpfzo  13828  elfznelfzo  13829  zmodid2  13960  2submod  13996  modfzo0difsn  14007  om2uzlti  14014  expcan  14233  hashvnfin  14424  hashneq0  14428  prhash2ex  14463  hashgt0elex  14465  hashgt12el  14487  hashgt12el2  14488  hashbclem  14517  hashf1lem2  14521  prprrab  14538  swrd0  14728  pfxn0  14756  swrdswrd  14774  pfxccat3  14803  repswswrd  14855  cshf1  14881  cshw1repsw  14894  relexpindlem  15136  sgnneg  15173  sgn3da  15174  absz  15398  iserex  15744  prodrb  16019  absdvdsb  16364  dvdsabsb  16365  modmulconst  16378  dvdsadd  16392  dvdsabseq  16403  mod2eq0even  16436  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  zeo5  16446  sadadd2lem2  16540  smupvallem  16573  gcdass  16637  lcmdvds  16698  lcmass  16704  divgcdcoprm0  16755  divgcdcoprmex  16756  1nprm  16769  dvdsnprmd  16780  prmdvdssq  16809  ncoprmlnprm  16819  isevengcd2  16821  m1dvdsndvds  16890  cshws0  17193  sbcie3s  17254  dfiso2  17861  initoid  18090  termoid  18091  funcestrcsetclem8  18235  lublecllem  18446  odudlatb  18613  sgrppropd  18833  issubm2  18912  mgm2nsgrplem2  19031  nsgacs  19285  cycsubg2  19338  gapm  19433  sscntz  19453  pgrpsubgsymgbi  19535  f1omvdcnv  19571  pmtrprfvalrn  19615  odval2  19678  lsmcntz  19806  rngpropd  20309  rnghmf1o  20593  isrngim2  20594  rhmf1o  20638  isrim  20639  df2idl2crng  21484  dfprm2  21686  pzriprnglem10  21703  psgnfix2  21812  islinds3  22047  islindf4  22051  snifpsrbag  22135  gsumply1eq  22534  mdetdiaglem  22820  mdetunilem9  22842  slesolinv  22905  slesolex  22907  cpmatel2  22938  m2cpmghm  22969  m2cpminvid2  22980  pm2mpf1  23024  chfacfscmul0  23083  chfacfscmulfsupp  23084  chfacfpmmul0  23087  chfacfpmmulfsupp  23088  isopn2  23257  cmpsub  23625  connsub  23646  ncvs1  25385  rrxmvallem  25632  itg1mulc  25932  lhop1  26241  mdegleb  26289  lawcos  27053  leibpi  27179  2lgslem1a  27627  2sq2  27669  lestric  28004  bdayons  28541  n0subs2  28629  bdaypw2n0bndlem  28728  angmgmaddov2  29268  colinearalg  29367  edg0iedg0  29512  uhgreq12g  29522  uhgrvtxedgiedgb  29593  usgredg2v  29687  edg0usgr  29713  dfnbgr2  29797  nbuhgr  29803  nbusgredgeu0  29828  nb3grprlem1  29840  nb3grpr  29842  uvtx2vtx1edgb  29859  redwlk  30130  uhgrwkspthlem2  30219  usgr2wlkspth  30224  pthdlem1  30231  cyclnspth  30268  crctcshwlkn0lem1  30278  crctcshwlkn0lem4  30281  crctcsh  30292  iswwlksnx  30308  wwlksm1edg  30349  wwlksnextsurj  30368  wwlksnextproplem3  30379  2wlkdlem4  30396  2wlkdlem5  30397  2pthdlem1  30398  s3wwlks2on  30424  sps3wwlks2on  30425  wpthswwlks2on  30432  elwspths2spth  30438  rusgrnumwwlks  30445  umgrclwwlkge2  30461  clwlkclwwlklem2a4  30467  clwlkclwwlk  30472  clwlkclwwlkflem  30474  clwwisshclwws  30485  isclwwlknx  30506  clwwlknwwlksnb  30525  eclclwwlkn1  30545  clwwlknonel  30565  clwwlknun  30582  3wlkdlem6  30645  frgrncvvdeqlem9  30787  fusgreg2wsp  30816  numclwwlk2lem1lem  30822  extwwlkfab  30832  frgrreggt1  30873  ubthlem1  31351  norm-i  31610  hoeq  32241  nmopgt0  32393  pjimai  32657  chirredi  32875  addltmulALT  32927  opreu2reuALT  32952  sbcies  32963  rmounid  32970  iunrdx  33037  disjrdx  33064  archiabl  33638  islbs5  33813  ist0cld  34343  oms0  34808  eulerpartgbij  34883  reprinrn  35126  usgrgt2cycl  35723  satfv1lem  35941  satf0op  35956  dmopab3rexdif  35984  satefvfmla0  35997  mrsubrn  36092  topfne  36973  unbdqndv1  37205  bj-hbntbi  37437  bj-issetwt  37618  bj-clel3gALT  37792  copsex2d  37891  bj-elid6  37922  dfgcd3  38076  topdifinfeq  38104  wl-sbalnae  38325  sin2h  38364  poimirlem16  38385  poimirlem17  38386  poimirlem25  38394  mbfresfi  38415  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  ftc1anclem1  38442  findcard4  38463  isidlc  38765  eldmressnALTV  39027  islshpsm  39853  lshpkrlem1  39983  opcon1b  40071  lautlt  40964  lauteq  40968  idlaut  40969  diblsmopel  42044  doch11  42246  recbothd  42858  aks4d1p8d2  42951  aks4d1p8  42953  isprimroot2  42960  posbezout  42966  aks6d1c5lem1  43002  sticksstones1  43012  sticksstones11  43022  sticksstones22  43034  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c7  43050  aks5lem8  43067  dvdsexpnn0  43209  redvmptabs  43235  redivne0bd  43325  prjsprellsp  43457  prjspeclsp  43458  abbibw  43523  istopclsd  43545  eqrabdioph  43622  rexzrexnn0  43645  zindbi  43787  expdiophlem2  43863  onsupeqmax  44087  onsupeqnmax  44088  ordeldif  44099  infordmin  44372  inintabd  44419  cnvcnvintabd  44440  cnvintabd  44443  sqrtcvallem1  44471  reabsifneg  44472  fsovrfovd  44849  ntrclsiso  44907  ntrneifv3  44922  ntrneineine0lem  44923  ntrneicls11  44930  suprleubrd  45006  suprlubrd  45008  lemuldiv4d  45011  pm14.122a  45246  3impexpbicomi  45304  onfrALTlem5  45365  bitr3VD  45671  onfrALTlem5VD  45707  csbrngVD  45718  pwpwuni  45891  supxrre3  46155  xrralrecnnge  46219  eliooshift  46336  limsupre2lem  46552  liminflimsupclim  46635  xlimbr  46655  smfrec  47617  fsetprcnexALT  47950  f1cof1b  47965  reuf1odnf  47995  2reuimp  48003  ralbinrald  48010  afvco2  48064  dfatdmfcoafv2  48142  recnmulnred  48193  sqrtnegnre  48195  subsubelfzo0  48215  ceilbi  48225  ichcircshi  48354  sprvalpwle2  48389  sprsymrelf1lem  48391  sbcpr  48421  poprelb  48424  31prm  48500  requad01  48537  dfeven3  48574  iseven5  48580  0noddALTV  48605  2noddALTV  48609  fpprmod  48643  sbgoldbaltlem1  48695  bgoldbtbndlem2  48722  dfclnbgr2  48739  dfsclnbgr2  48762  dfvopnbgr2  48769  dfsclnbgr6  48774  isuspgrim0lem  48809  usgrgrtrirex  48866  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgn4cyclex  49042  0nodd  49085  2nodd  49087  isassintop  49125  uzlidlring  49150  funcringcsetcALTV2lem8  49212  funcringcsetclem8ALTV  49235  prmringnzring  49252  dfidom2  49258  idomcanl  49262  nn0sumltlt  49280  ply1mulgsumlem2  49317  islindeps  49383  lindslinindsimp1  49387  lindslinindsimp2  49393  snlindsntor  49401  zlmodzxznm  49427  ldepslinc  49439  elbigo2  49482  elbigolo1  49487  logblt1b  49494  fldivexpfllog2  49495  nnolog2flm1  49520  digexp  49537  nn0sumshdiglemB  49550  itsclquadeu  49707  itscnhlinecirc02p  49715  ipolublem  49912  ipoglblem  49915  dvsec  50689  dvcsc  50690  dvcot  50691  ralrals  50737  rexrals  50738  ralals  50743  rexals  50744