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 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced 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  545  rbaib  547  baibd  548  anabs5  675  annotanannot  847  pm5.55  963  pm5.54  1033  ninba  1037  pm5.75  1044  sbequ12r  2294  sbal1  2566  euor2  2647  eqabcdv  2903  necon3bbid  3001  necon4bbid  3005  ralanid  3119  rexanid  3120  sbralieALT  3350  ralcom2  3373  rmoanid  3386  reuanid  3387  rabrabi  3442  gencbvex  3519  alexeqg  3619  clel2g  3627  clel3g  3629  clel4g  3631  reurab  3673  reu8  3705  sbceq2a  3765  sbcco2  3780  reu8nf  3839  notabw  4274  2reu4lem  4489  reurexprg  4675  raltpd  4752  ssdifsn  4760  uniprg  4892  disjxun  5111  opabidw  5509  opabid  5510  soeq2  5592  sotrine  5610  posn  5748  xpiindi  5822  dmopab2rex  5908  elpredg  6317  fvopab6  7025  cbvfo  7288  f1eqcocnv  7300  isoid  7328  isoini  7337  isosolem  7346  riotaeqimp  7394  riotarab  7410  resoprab2  7530  tfisi  7855  tfinds2  7860  f1oweALT  7969  dfoprab3  8051  opiota  8056  mpof1o2d  8121  xpord2indlem  8143  xpord3inddlem  8150  mpocurryd  8265  oalimcl  8545  omword  8555  oeword  8576  nnacan  8614  nnmcan  8620  mapsnd  8884  findcard2s  9150  funisfsupp  9327  suppeqfsuppbi  9339  eqinf  9445  inflb  9450  infglb  9451  infglbb  9452  infltoreq  9464  infempty  9469  brwdomn0  9531  cantnfp1lem3  9649  ssrankr1  9807  r1pw  9817  djulf1o  9898  djurf1o  9899  aleph11  10068  alephval3  10094  gch-kn  10662  wunex2  10723  lttri2  11292  wloglei  11746  divne0b  11883  lemul1  12067  nnnle0  12269  div4p1lem1div2  12499  nn0ind-raph  12696  zindd  12697  suprfinzcl  12710  rebtwnz  12971  qreccl  12993  elpq  12999  xrlttri2  13167  2resupmax  13214  xmulneg1  13295  iooshf  13453  difreicc  13511  fzofzim  13738  elfzomelpfzo  13801  elfznelfzo  13802  zmodid2  13932  2submod  13968  modfzo0difsn  13979  om2uzlti  13986  expcan  14205  hashvnfin  14396  hashneq0  14400  prhash2ex  14435  hashgt0elex  14437  hashgt12el  14459  hashgt12el2  14460  hashbclem  14489  hashf1lem2  14493  prprrab  14510  swrd0  14696  pfxn0  14724  swrdswrd  14742  pfxccat3  14771  repswswrd  14821  cshf1  14847  cshw1repsw  14860  relexpindlem  15100  sgnneg  15137  sgn3da  15138  absz  15362  iserex  15708  prodrb  15986  absdvdsb  16332  dvdsabsb  16333  modmulconst  16346  dvdsadd  16360  dvdsabseq  16371  mod2eq0even  16404  oddnn02np1  16406  oddge22np1  16407  evennn02n  16408  evennn2n  16409  zeo5  16414  sadadd2lem2  16508  smupvallem  16541  gcdass  16605  lcmdvds  16666  lcmass  16672  divgcdcoprm0  16723  divgcdcoprmex  16724  1nprm  16737  dvdsnprmd  16748  prmdvdssq  16777  ncoprmlnprm  16787  isevengcd2  16789  m1dvdsndvds  16858  cshws0  17161  sbcie3s  17222  dfiso2  17829  initoid  18058  termoid  18059  funcestrcsetclem8  18203  lublecllem  18414  odudlatb  18581  sgrppropd  18789  issubm2  18862  mgm2nsgrplem2  18981  nsgacs  19228  cycsubg2  19281  gapm  19376  sscntz  19396  pgrpsubgsymgbi  19478  f1omvdcnv  19514  pmtrprfvalrn  19558  odval2  19621  lsmcntz  19749  rngpropd  20252  rnghmf1o  20534  isrngim2  20535  rhmf1o  20573  isrim  20574  df2idl2crng  21392  dfprm2  21592  pzriprnglem10  21609  psgnfix2  21718  islinds3  21953  islindf4  21957  snifpsrbag  22039  gsumply1eq  22438  mdetdiaglem  22724  mdetunilem9  22746  slesolinv  22806  slesolex  22808  cpmatel2  22839  m2cpmghm  22870  m2cpminvid2  22881  pm2mpf1  22925  chfacfscmul0  22984  chfacfscmulfsupp  22985  chfacfpmmul0  22988  chfacfpmmulfsupp  22989  isopn2  23158  cmpsub  23526  connsub  23547  ncvs1  25285  rrxmvallem  25532  itg1mulc  25832  lhop1  26142  mdegleb  26190  lawcos  26947  leibpi  27073  2lgslem1a  27521  2sq2  27563  lestric  27898  bdayons  28435  n0subs2  28523  bdaypw2n0bndlem  28622  colinearalg  29201  edg0iedg0  29346  uhgreq12g  29356  uhgrvtxedgiedgb  29427  usgredg2v  29518  edg0usgr  29544  dfnbgr2  29628  nbuhgr  29634  nbusgredgeu0  29659  nb3grprlem1  29671  nb3grpr  29673  uvtx2vtx1edgb  29690  redwlk  29961  uhgrwkspthlem2  30044  usgr2wlkspth  30049  pthdlem1  30056  cyclnspth  30091  crctcshwlkn0lem1  30100  crctcshwlkn0lem4  30103  crctcsh  30114  iswwlksnx  30130  wwlksm1edg  30171  wwlksnextsurj  30190  wwlksnextproplem3  30201  2wlkdlem4  30218  2wlkdlem5  30219  2pthdlem1  30220  s3wwlks2on  30246  sps3wwlks2on  30247  wpthswwlks2on  30254  elwspths2spth  30260  rusgrnumwwlks  30267  umgrclwwlkge2  30283  clwlkclwwlklem2a4  30289  clwlkclwwlk  30294  clwlkclwwlkflem  30296  clwwisshclwws  30307  isclwwlknx  30328  clwwlknwwlksnb  30347  eclclwwlkn1  30367  clwwlknonel  30387  clwwlknun  30404  3wlkdlem6  30457  frgrncvvdeqlem9  30599  fusgreg2wsp  30628  numclwwlk2lem1lem  30634  extwwlkfab  30644  frgrreggt1  30685  ubthlem1  31163  norm-i  31422  hoeq  32053  nmopgt0  32205  pjimai  32469  chirredi  32687  addltmulALT  32739  opreu2reuALT  32764  sbcies  32775  rmounid  32782  iunrdx  32849  disjrdx  32877  archiabl  33459  islbs5  33637  ist0cld  34168  oms0  34632  eulerpartgbij  34707  reprinrn  34950  usgrgt2cycl  35521  satfv1lem  35753  satf0op  35768  dmopab3rexdif  35796  satefvfmla0  35809  mrsubrn  35904  topfne  36754  unbdqndv1  36986  bj-hbntbi  37218  bj-issetwt  37399  bj-clel3gALT  37572  copsex2d  37671  bj-elid6  37702  dfgcd3  37856  topdifinfeq  37884  wl-sbalnae  38105  sin2h  38149  poimirlem16  38175  poimirlem17  38176  poimirlem25  38184  mbfresfi  38205  itg2addnclem  38210  itg2addnclem2  38211  itg2addnclem3  38212  ftc1anclem1  38232  isidlc  38554  eldmressnALTV  38818  islshpsm  39644  lshpkrlem1  39774  opcon1b  39862  lautlt  40755  lauteq  40759  idlaut  40760  diblsmopel  41835  doch11  42037  recbothd  42649  aks4d1p8d2  42742  aks4d1p8  42744  isprimroot2  42751  posbezout  42757  aks6d1c5lem1  42793  sticksstones1  42803  sticksstones11  42813  sticksstones22  42825  aks6d1c6lem3  42829  aks6d1c6lem4  42830  aks6d1c7  42841  aks5lem8  42858  dvdsexpnn0  42985  redvmptabs  43011  redivne0bd  43101  prjsprellsp  43235  prjspeclsp  43236  abbibw  43301  istopclsd  43323  eqrabdioph  43400  rexzrexnn0  43423  zindbi  43565  expdiophlem2  43641  onsupeqmax  43865  onsupeqnmax  43866  ordeldif  43877  infordmin  44150  inintabd  44197  cnvcnvintabd  44218  cnvintabd  44221  sqrtcvallem1  44249  reabsifneg  44250  fsovrfovd  44627  ntrclsiso  44685  ntrneifv3  44700  ntrneineine0lem  44701  ntrneicls11  44708  suprleubrd  44784  suprlubrd  44786  lemuldiv4d  44789  pm14.122a  45024  3impexpbicomi  45082  onfrALTlem5  45143  bitr3VD  45449  onfrALTlem5VD  45485  csbrngVD  45496  pwpwuni  45669  supxrre3  45933  xrralrecnnge  45997  eliooshift  46114  limsupre2lem  46330  liminflimsupclim  46413  xlimbr  46433  smfrec  47395  fsetprcnexALT  47688  f1cof1b  47703  reuf1odnf  47733  2reuimp  47741  ralbinrald  47748  afvco2  47802  dfatdmfcoafv2  47880  recnmulnred  47931  sqrtnegnre  47933  subsubelfzo0  47953  ceilbi  47963  ichcircshi  48092  sprvalpwle2  48127  sprsymrelf1lem  48129  sbcpr  48159  poprelb  48162  31prm  48238  requad01  48275  dfeven3  48312  iseven5  48318  0noddALTV  48343  2noddALTV  48347  fpprmod  48381  sbgoldbaltlem1  48433  bgoldbtbndlem2  48460  dfclnbgr2  48477  dfsclnbgr2  48500  dfvopnbgr2  48507  dfsclnbgr6  48512  isuspgrim0lem  48547  usgrgrtrirex  48604  usgrexmpl2nb1  48686  usgrexmpl2nb2  48687  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  pgnbgreunbgrlem2lem3  48770  pgn4cyclex  48780  0nodd  48824  2nodd  48826  isassintop  48864  uzlidlring  48889  funcringcsetcALTV2lem8  48951  funcringcsetclem8ALTV  48974  prmringnzring  48991  dfidom2  48997  nn0sumltlt  49015  ply1mulgsumlem2  49052  islindeps  49118  lindslinindsimp1  49122  lindslinindsimp2  49128  snlindsntor  49136  zlmodzxznm  49162  ldepslinc  49174  elbigo2  49217  elbigolo1  49222  logblt1b  49229  fldivexpfllog2  49230  nnolog2flm1  49255  digexp  49272  nn0sumshdiglemB  49285  itsclquadeu  49442  itscnhlinecirc02p  49450  ipolublem  49649  ipoglblem  49652