Theorem bicomd 225

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  impbid2  228  syl5ibr  248  ibir  270  bitr2d  282  bitr3d  283  bitr4d  284  syl5rbb  286  syl6rbb  290  con1bid  358  pm5.5  364  imnot  368  baibr  539  rbaib  541  baibd  542  anabs5  661  annotanannot  832  pm5.55  945  pm5.54  1014  ninba  1018  pm5.75  1025  norassOLD  1534  sbequ12r  2254  cbvalvOLD  2420  sbal1  2572  euor2  2697  abbi1dv  2952  necon3bbid  3053  necon4bbid  3057  ralanid  3168  rexanid  3252  ralcom2  3363  sbralie  3471  gencbvex  3549  sbhypf  3552  alexeqg  3644  clel2g  3652  clel3g  3654  reu8  3724  sbceq2a  3784  sbcco2  3799  reu8nf  3860  2reu4lem  4465  reurexprg  4640  raltpd  4716  ssdifsn  4720  disjxun  5064  opabidw  5412  opabid  5413  soeq2  5495  posn  5637  xpiindi  5706  dmopab2rex  5786  fvopab6  6801  cbvfo  7045  f1eqcocnv  7057  isoid  7082  isoini  7091  isosolem  7100  riotaeqimp  7140  resoprab2  7271  tfisi  7573  tfinds2  7578  f1oweALT  7673  dfoprab3  7752  opiota  7757  mpocurryd  7935  oalimcl  8186  omword  8196  oeword  8216  nnacan  8254  nnmcan  8260  mapsnd  8450  findcard2s  8759  funisfsupp  8838  suppeqfsuppbi  8847  eqinf  8948  inflb  8953  infglb  8954  infglbb  8955  infltoreq  8966  infempty  8971  brwdomn0  9033  cantnfp1lem3  9143  ssrankr1  9264  r1pw  9274  djulf1o  9341  djurf1o  9342  aleph11  9510  alephval3  9536  gch-kn  10099  wunex2  10160  lttri2  10723  wloglei  11172  divne0b  11309  lemul1  11492  nnnle0  11671  div4p1lem1div2  11893  nn0ind-raph  12083  zindd  12084  suprfinzcl  12098  rebtwnz  12348  qreccl  12369  elpq  12375  xrlttri2  12536  2resupmax  12582  xmulneg1  12663  iooshf  12816  difreicc  12871  fzofzim  13085  elfzomelpfzo  13142  elfznelfzo  13143  zmodid2  13268  2submod  13301  modfzo0difsn  13312  om2uzlti  13319  expcan  13534  hashvnfin  13722  hashneq0  13726  prhash2ex  13761  hashgt0elex  13763  hashgt12el  13784  hashgt12el2  13785  hashbclem  13811  hashf1lem2  13815  prprrab  13832  swrd0  14020  pfxn0  14048  swrdswrd  14067  pfxccat3  14096  repswswrd  14146  cshf1  14172  cshw1repsw  14185  relexpindlem  14422  absz  14671  iserex  15013  prodrb  15286  absdvdsb  15628  dvdsabsb  15629  modmulconst  15641  dvdsadd  15652  dvdsabseq  15663  mod2eq0even  15695  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  zeo5  15705  sadadd2lem2  15799  smupvallem  15832  gcdass  15895  lcmdvds  15952  lcmass  15958  divgcdcoprm0  16009  divgcdcoprmex  16010  1nprm  16023  dvdsnprmd  16034  ncoprmlnprm  16068  isevengcd2  16070  m1dvdsndvds  16135  cshws0  16435  sbcie2s  16540  sbcie3s  16541  dfiso2  17042  initoid  17265  termoid  17266  funcestrcsetclem8  17397  lublecllem  17598  odudlatb  17806  issubm2  17969  mgm2nsgrplem2  18084  nsgacs  18314  cycsubg2  18353  gapm  18436  sscntz  18456  pgrpsubgsymgbi  18536  f1omvdcnv  18572  pmtrprfvalrn  18616  odval2  18679  lsmcntz  18805  rhmf1o  19484  isrim  19485  snifpsrbag  20146  gsumply1eq  20473  dfprm2  20641  psgnfix2  20743  islinds3  20978  islindf4  20982  mdetdiaglem  21207  mdetunilem9  21229  slesolinv  21289  slesolex  21291  cpmatel2  21321  m2cpmghm  21352  m2cpminvid2  21363  pm2mpf1  21407  chfacfscmul0  21466  chfacfscmulfsupp  21467  chfacfpmmul0  21470  chfacfpmmulfsupp  21471  isopn2  21640  cmpsub  22008  connsub  22029  ncvs1  23761  rrxmvallem  24007  itg1mulc  24305  lhop1  24611  mdegleb  24658  lawcos  25394  leibpi  25520  2lgslem1a  25967  2sq2  26009  iscgra  26595  colinearalg  26696  edg0iedg0  26840  uhgreq12g  26850  uhgrvtxedgiedgb  26921  usgredg2v  27009  edg0usgr  27035  dfnbgr2  27119  nbuhgr  27125  nbusgredgeu0  27150  nb3grprlem1  27162  nb3grpr  27164  uvtx2vtx1edgb  27181  redwlk  27454  uhgrwkspthlem2  27535  usgr2wlkspth  27540  pthdlem1  27547  cyclnspth  27581  crctcshwlkn0lem1  27588  crctcshwlkn0lem4  27591  crctcsh  27602  iswwlksnx  27618  wwlksm1edg  27659  wwlksnextsurj  27678  wwlksnextproplem3  27690  2wlkdlem4  27707  2wlkdlem5  27708  2pthdlem1  27709  s3wwlks2on  27735  wpthswwlks2on  27740  elwspths2spth  27746  rusgrnumwwlks  27753  umgrclwwlkge2  27769  clwlkclwwlklem2a4  27775  clwlkclwwlk  27780  clwlkclwwlkflem  27782  clwwisshclwws  27793  isclwwlknx  27814  clwwlknwwlksnb  27834  eclclwwlkn1  27854  clwwlknonel  27874  clwwlknun  27891  3wlkdlem6  27944  frgrncvvdeqlem9  28086  fusgreg2wsp  28115  numclwwlk2lem1lem  28121  extwwlkfab  28131  frgrreggt1  28172  ubthlem1  28647  norm-i  28906  hoeq  29537  nmopgt0  29689  pjimai  29953  chirredi  30171  addltmulALT  30223  opreu2reuALT  30240  sbcies  30251  rmounid  30259  iunrdx  30315  disjrdx  30341  cnvoprabOLD  30456  archiabl  30827  oms0  31555  eulerpartgbij  31630  sgnneg  31798  sgn3da  31799  reprinrn  31889  usgrgt2cycl  32377  satfv1lem  32609  satf0op  32624  dmopab3rexdif  32652  satefvfmla0  32665  mrsubrn  32760  sotrine  33003  etasslt  33274  topfne  33702  unbdqndv1  33847  bj-hbntbi  34038  bj-issetwt  34192  copsex2d  34434  bj-elid6  34465  dfgcd3  34608  topdifinfeq  34634  wl-sb6rft  34799  wl-sbalnae  34813  wl-dfralf  34854  sin2h  34897  poimirlem16  34923  poimirlem17  34924  poimirlem25  34932  mbfresfi  34953  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  ftc1anclem1  34982  isidlc  35308  islshpsm  36131  lshpkrlem1  36261  opcon1b  36349  lautlt  37242  lauteq  37246  idlaut  37247  diblsmopel  38322  doch11  38524  rabeqcda  39126  prjsprellsp  39281  prjspeclsp  39282  istopclsd  39317  eqrabdioph  39394  rexzrexnn0  39421  zindbi  39563  expdiophlem2  39639  infordmin  39919  inintabd  39959  cnvcnvintabd  39980  cnvintabd  39983  fsovrfovd  40375  ntrclsiso  40437  ntrneifv3  40452  ntrneineine0lem  40453  ntrneicls11  40460  suprleubrd  40537  suprlubrd  40540  lemuldiv4d  40543  pm14.122a  40774  3impexpbicomi  40834  onfrALTlem5  40896  bitr3VD  41203  onfrALTlem5VD  41239  csbrngVD  41250  pwpwuni  41339  supxrre3  41613  xrralrecnnge  41682  eliooshift  41802  limsupre2lem  42025  liminflimsupclim  42108  xlimbr  42128  smfrec  43084  reuf1odnf  43326  2reuimp  43334  ralbinrald  43341  afvco2  43395  dfatdmfcoafv2  43473  recnmulnred  43525  sqrtnegnre  43527  subsubelfzo0  43546  ichcircshi  43632  sprvalpwle2  43671  sprsymrelf1lem  43673  sbcpr  43703  poprelb  43706  31prm  43780  requad01  43806  dfeven3  43843  iseven5  43849  0noddALTV  43874  2noddALTV  43878  fpprmod  43912  sbgoldbaltlem1  43964  bgoldbtbndlem2  43991  isomuspgrlem2d  44016  0nodd  44097  2nodd  44099  isassintop  44137  rnghmf1o  44194  isrngim  44195  uzlidlring  44220  funcringcsetcALTV2lem8  44334  funcringcsetclem8ALTV  44357  nn0sumltlt  44418  ply1mulgsumlem2  44461  islindeps  44528  lindslinindsimp1  44532  lindslinindsimp2  44538  snlindsntor  44546  zlmodzxznm  44572  ldepslinc  44584  difmodm1lt  44602  elbigo2  44632  elbigolo1  44637  logblt1b  44644  fldivexpfllog2  44645  nnolog2flm1  44670  digexp  44687  nn0sumshdiglemB  44700  itsclquadeu  44784  itscnhlinecirc02p  44792