Theorem bicomd 213

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  impbid2  216  syl5ibr  236  ibir  257  bitr2d  269  bitr3d  270  bitr4d  271  syl5rbb  273  syl6rbb  277  con1bid  345  pm5.5  351  imnot  355  anabs5  851  pm5.55  939  pm5.54  943  baibr  945  rbaib  947  baibd  948  rbaibd  949  ninba  965  pm5.75  978  pm5.75OLD  979  sbequ12r  2112  cbvalv  2273  sbal1  2460  euor2  2514  abbi1dv  2743  necon3bbid  2831  necon4bbid  2835  ralcom2  3104  gencbvex  3250  sbhypf  3253  alexeqg  3332  clel3g  3340  reu8  3402  sbceq2a  3447  sbcco2  3459  reu8nf  3516  raltpd  4315  disjxun  4651  opabid  4982  soeq2  5055  posn  5187  xpiindi  5257  fvopab6  6310  cbvfo  6544  f1eqcocnv  6556  isoid  6579  isoini  6588  isosolem  6597  riotaeqimp  6634  resoprab2  6757  tfisi  7058  tfinds2  7063  f1oweALT  7152  dfoprab3  7224  opiota  7229  mpt2curryd  7395  oalimcl  7640  omword  7650  oeword  7670  nnacan  7708  nnmcan  7714  findcard2s  8201  funisfsupp  8280  suppeqfsuppbi  8289  eqinf  8390  inflb  8395  infglb  8396  infglbb  8397  infltoreq  8408  infempty  8412  brwdomn0  8474  cantnfp1lem3  8577  ssrankr1  8698  r1pw  8708  aleph11  8907  alephval3  8933  gch-kn  9499  wunex2  9560  lttri2  10120  wloglei  10560  divne0b  10696  lemul1  10875  nnnle0  11051  div4p1lem1div2  11287  nn0ind-raph  11477  zindd  11478  suprfinzcl  11492  rebtwnz  11787  qreccl  11808  xrlttri2  11975  2resupmax  12019  xmulneg1  12099  iooshf  12252  difreicc  12304  fzofzim  12514  elfzomelpfzo  12572  elfznelfzo  12573  divfl0  12625  zmodid2  12698  2submod  12731  modfzo0difsn  12742  om2uzlti  12749  expcan  12913  hashvnfin  13151  hashneq0  13155  prhash2ex  13187  hashgt0elex  13189  hashgt12el  13210  hashgt12el2  13211  hashbclem  13236  hashf1lem2  13240  prprrab  13255  swrdn0  13430  swrd0  13434  2swrdeqwrdeq  13453  swrdswrd  13460  swrdccat3  13492  repswswrd  13531  cshf1  13556  cshw1repsw  13569  relexpindlem  13803  absz  14051  iserex  14387  prodrb  14662  absdvdsb  15000  dvdsabsb  15001  modmulconst  15013  dvdsadd  15024  dvdsabseq  15035  mod2eq0even  15070  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  zeo5  15080  sadadd2lem2  15172  smupvallem  15205  gcdass  15264  lcmdvds  15321  lcmass  15327  divgcdcoprm0  15379  divgcdcoprmex  15380  1nprm  15392  dvdsnprmd  15403  ncoprmlnprm  15436  isevengcd2  15438  m1dvdsndvds  15503  cshws0  15808  sbcie2s  15916  sbcie3s  15917  dfiso2  16432  initoid  16655  termoid  16656  funcestrcsetclem8  16787  lublecllem  16988  odudlatb  17196  issubm2  17348  mgm2nsgrplem2  17406  nsgacs  17630  cycsubg2  17631  gapm  17739  sscntz  17759  pgrpsubgsymgbi  17827  f1omvdcnv  17864  pmtrprfvalrn  17908  odval2  17970  lsmcntz  18092  rhmf1o  18732  isrim  18733  snifpsrbag  19366  gsumply1eq  19675  dfprm2  19842  psgnfix2  19945  islinds3  20173  islindf4  20177  mdetdiaglem  20404  mdetunilem9  20426  slesolinv  20486  slesolex  20488  cpmatel2  20518  m2cpmghm  20549  m2cpminvid2  20560  pm2mpf1  20604  chfacfscmul0  20663  chfacfscmulfsupp  20664  chfacfpmmul0  20667  chfacfpmmulfsupp  20668  isopn2  20836  cmpsub  21203  connsub  21224  ncvs1  22957  rrxmvallem  23187  itg1mulc  23471  lhop1  23777  mdegleb  23824  lawcos  24546  leibpi  24669  2lgslem1a  25116  iscgra  25701  colinearalg  25790  edg0iedg0  25949  edg0iedg0OLD  25950  uhgreq12g  25960  uhgrvtxedgiedgb  26031  usgredg2v  26119  edg0usgr  26145  dfnbgr2  26235  nbuhgr  26239  nbusgredgeu0  26270  nb3grprlem1  26282  nb3grpr  26284  uvtx2vtx1edgb  26300  upgrewlkle2  26502  wlkeq  26529  redwlk  26569  uhgrwkspthlem2  26650  usgr2wlkspth  26655  pthdlem1  26662  cyclnspth  26695  crctcshwlkn0lem1  26702  crctcshwlkn0lem4  26705  crctcsh  26716  iswwlksnx  26731  wlkiswwlksupgr2  26763  wwlksm1edg  26767  wwlksnextsur  26795  wwlksnextproplem3  26806  wwlksnwwlksnon  26810  2wlkdlem4  26824  2wlkdlem5  26825  2pthdlem1  26826  s3wwlks2on  26849  wpthswwlks2on  26854  usgr2wspthons3  26857  elwspths2spth  26862  rusgrnumwwlks  26869  isclwwlksnx  26889  clwlkclwwlklem2a4  26898  clwlkclwwlk  26903  umgrclwwlksge2  26912  clwwisshclwws  26928  eclclwwlksn1  26952  clwlksfoclwwlk  26963  clwwlksnun  26974  3wlkdlem6  27025  frgrncvvdeqlem9  27171  fusgreg2wsp  27200  clwwlkextfrlem1  27208  extwwlkfab  27223  frgrreggt1  27251  ubthlem1  27726  norm-i  27986  hoeq  28619  nmopgt0  28771  pjimai  29035  chirredi  29253  addltmulALT  29305  sbcies  29322  iunrdx  29382  disjrdx  29404  cnvoprab  29498  archiabl  29752  oms0  30359  eulerpartgbij  30434  sgnneg  30602  sgn3da  30603  reprinrn  30696  mrsubrn  31410  sotrine  31658  etasslt  31920  topfne  32349  unbdqndv1  32499  bj-hbntbi  32695  bj-abbi1dv  32781  bj-issetwt  32859  dfgcd3  33170  topdifinfeq  33198  wl-sb6rft  33330  wl-sbalnae  33345  sin2h  33399  poimirlem16  33425  poimirlem17  33426  poimirlem25  33434  mbfresfi  33456  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  ftc1anclem1  33485  isidlc  33814  islshpsm  34267  lshpkrlem1  34397  opcon1b  34485  lautlt  35377  lauteq  35381  idlaut  35382  diblsmopel  36460  doch11  36662  istopclsd  37263  eqrabdioph  37341  rexzrexnn0  37368  zindbi  37511  expdiophlem2  37589  inintabd  37885  cnvcnvintabd  37906  cnvintabd  37909  fsovrfovd  38303  ntrclsiso  38365  ntrneifv3  38380  ntrneineine0lem  38381  ntrneicls11  38388  suprleubrd  38466  suprlubrd  38470  lemuldiv4d  38473  pm14.122a  38623  3impexpbicomi  38686  onfrALTlem5  38757  bitr3VD  39084  onfrALTlem5VD  39121  csbrngVD  39132  pwpwuni  39225  mapsnd  39388  supxrre3  39541  xrralrecnnge  39613  eliooshift  39729  limsupre2lem  39956  liminflimsupclim  40039  xlimbr  40053  smfrec  40996  2reu4a  41189  ralbinrald  41199  afvco2  41256  subsubelfzo0  41336  pfxsuffeqwrdeq  41406  pfxccat3  41426  31prm  41512  dfeven3  41570  iseven5  41576  0noddALTV  41600  2noddALTV  41604  sbgoldbaltlem1  41667  bgoldbtbndlem2  41694  sprvalpwle2  41739  sprsymrelf1lem  41741  0nodd  41810  2nodd  41812  isassintop  41846  rnghmf1o  41903  isrngim  41904  uzlidlring  41929  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  nn0sumltlt  42128  ply1mulgsumlem2  42175  islindeps  42242  lindslinindsimp1  42246  lindslinindsimp2  42252  snlindsntor  42260  zlmodzxznm  42286  ldepslinc  42298  difmodm1lt  42317  elbigo2  42346  elbigolo1  42351  logblt1b  42358  fldivexpfllog2  42359  nnolog2flm1  42384  digexp  42401  nn0sumshdiglemB  42414