Theorem bicomd 223

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  impbid2  226  imbitrrid  246  ibir  268  bitr2d  280  bitr3d  281  bitr4d  282  bitr2id  284  bitr2di  288  con1bid  355  pm5.5  361  imnot  365  baibr  536  rbaib  538  baibd  539  anabs5  664  annotanannot  835  pm5.55  951  pm5.54  1020  ninba  1024  pm5.75  1031  sbequ12r  2260  sbal1  2532  euor2  2613  eqabcdv  2870  necon3bbid  2969  necon4bbid  2973  ralanid  3085  rexanid  3086  sbralieALT  3316  ralcom2  3339  rmoanid  3352  reuanid  3353  rabrabi  3408  gencbvex  3487  alexeqg  3593  clel2g  3601  clel3g  3603  clel4g  3605  reurab  3647  reu8  3679  sbceq2a  3740  sbcco2  3755  reu8nf  3815  notabw  4253  2reu4lem  4463  reurexprg  4648  raltpd  4725  ssdifsn  4733  uniprg  4866  disjxun  5083  opabidw  5479  opabid  5480  soeq2  5561  sotrine  5579  posn  5717  xpiindi  5790  dmopab2rex  5872  elpredg  6279  fvopab6  6982  cbvfo  7244  f1eqcocnv  7256  isoid  7284  isoini  7293  isosolem  7302  riotaeqimp  7350  riotarab  7366  resoprab2  7486  tfisi  7810  tfinds2  7815  f1oweALT  7925  dfoprab3  8007  opiota  8012  xpord2indlem  8097  xpord3inddlem  8104  mpocurryd  8219  oalimcl  8495  omword  8505  oeword  8526  nnacan  8564  nnmcan  8570  mapsnd  8834  findcard2s  9100  funisfsupp  9280  suppeqfsuppbi  9292  eqinf  9398  inflb  9403  infglb  9404  infglbb  9405  infltoreq  9417  infempty  9422  brwdomn0  9484  cantnfp1lem3  9601  ssrankr1  9759  r1pw  9769  djulf1o  9836  djurf1o  9837  aleph11  10006  alephval3  10032  gch-kn  10600  wunex2  10661  lttri2  11228  wloglei  11682  divne0b  11820  lemul1  12007  nnnle0  12210  div4p1lem1div2  12432  nn0ind-raph  12629  zindd  12630  suprfinzcl  12643  rebtwnz  12897  qreccl  12919  elpq  12925  xrlttri2  13093  2resupmax  13140  xmulneg1  13221  iooshf  13379  difreicc  13437  fzofzim  13664  elfzomelpfzo  13727  elfznelfzo  13728  zmodid2  13858  2submod  13894  modfzo0difsn  13905  om2uzlti  13912  expcan  14131  hashvnfin  14322  hashneq0  14326  prhash2ex  14361  hashgt0elex  14363  hashgt12el  14384  hashgt12el2  14385  hashbclem  14414  hashf1lem2  14418  prprrab  14435  swrd0  14621  pfxn0  14649  swrdswrd  14667  pfxccat3  14696  repswswrd  14746  cshf1  14772  cshw1repsw  14785  relexpindlem  15025  absz  15273  iserex  15619  prodrb  15897  absdvdsb  16243  dvdsabsb  16244  modmulconst  16257  dvdsadd  16271  dvdsabseq  16282  mod2eq0even  16315  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  zeo5  16325  sadadd2lem2  16419  smupvallem  16452  gcdass  16516  lcmdvds  16577  lcmass  16583  divgcdcoprm0  16634  divgcdcoprmex  16635  1nprm  16648  dvdsnprmd  16659  prmdvdssq  16688  ncoprmlnprm  16698  isevengcd2  16700  m1dvdsndvds  16769  cshws0  17072  sbcie3s  17132  dfiso2  17739  initoid  17968  termoid  17969  funcestrcsetclem8  18113  lublecllem  18324  odudlatb  18491  sgrppropd  18699  issubm2  18772  mgm2nsgrplem2  18890  nsgacs  19137  cycsubg2  19185  gapm  19281  sscntz  19301  pgrpsubgsymgbi  19383  f1omvdcnv  19419  pmtrprfvalrn  19463  odval2  19526  lsmcntz  19654  rngpropd  20155  rnghmf1o  20432  isrngim2  20433  rhmf1o  20470  isrim  20471  dfprm2  21453  pzriprnglem10  21470  psgnfix2  21579  islinds3  21814  islindf4  21818  snifpsrbag  21900  gsumply1eq  22274  mdetdiaglem  22563  mdetunilem9  22585  slesolinv  22645  slesolex  22647  cpmatel2  22678  m2cpmghm  22709  m2cpminvid2  22720  pm2mpf1  22764  chfacfscmul0  22823  chfacfscmulfsupp  22824  chfacfpmmul0  22827  chfacfpmmulfsupp  22828  isopn2  22997  cmpsub  23365  connsub  23386  ncvs1  25124  rrxmvallem  25371  itg1mulc  25671  lhop1  25981  mdegleb  26029  lawcos  26780  leibpi  26906  2lgslem1a  27354  2sq2  27396  lestric  27732  bdayons  28268  n0subs2  28356  bdaypw2n0bndlem  28455  colinearalg  28979  edg0iedg0  29124  uhgreq12g  29134  uhgrvtxedgiedgb  29205  usgredg2v  29296  edg0usgr  29322  dfnbgr2  29406  nbuhgr  29412  nbusgredgeu0  29437  nb3grprlem1  29449  nb3grpr  29451  uvtx2vtx1edgb  29468  redwlk  29739  uhgrwkspthlem2  29822  usgr2wlkspth  29827  pthdlem1  29834  cyclnspth  29869  crctcshwlkn0lem1  29878  crctcshwlkn0lem4  29881  crctcsh  29892  iswwlksnx  29908  wwlksm1edg  29949  wwlksnextsurj  29968  wwlksnextproplem3  29979  2wlkdlem4  29996  2wlkdlem5  29997  2pthdlem1  29998  s3wwlks2on  30024  sps3wwlks2on  30025  wpthswwlks2on  30032  elwspths2spth  30038  rusgrnumwwlks  30045  umgrclwwlkge2  30061  clwlkclwwlklem2a4  30067  clwlkclwwlk  30072  clwlkclwwlkflem  30074  clwwisshclwws  30085  isclwwlknx  30106  clwwlknwwlksnb  30125  eclclwwlkn1  30145  clwwlknonel  30165  clwwlknun  30182  3wlkdlem6  30235  frgrncvvdeqlem9  30377  fusgreg2wsp  30406  numclwwlk2lem1lem  30412  extwwlkfab  30422  frgrreggt1  30463  ubthlem1  30941  norm-i  31200  hoeq  31831  nmopgt0  31983  pjimai  32247  chirredi  32465  addltmulALT  32517  opreu2reuALT  32546  sbcies  32557  rmounid  32564  iunrdx  32633  disjrdx  32661  sgnneg  32906  sgn3da  32907  archiabl  33259  islbs5  33440  ist0cld  33977  oms0  34441  eulerpartgbij  34516  reprinrn  34762  usgrgt2cycl  35312  satfv1lem  35544  satf0op  35559  dmopab3rexdif  35587  satefvfmla0  35600  mrsubrn  35695  topfne  36536  unbdqndv1  36768  bj-hbntbi  37001  bj-issetwt  37182  bj-clel3gALT  37355  copsex2d  37453  bj-elid6  37484  dfgcd3  37638  topdifinfeq  37666  wl-sbalnae  37887  sin2h  37931  poimirlem16  37957  poimirlem17  37958  poimirlem25  37966  mbfresfi  37987  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  ftc1anclem1  38014  isidlc  38336  eldmressnALTV  38600  islshpsm  39426  lshpkrlem1  39556  opcon1b  39644  lautlt  40537  lauteq  40541  idlaut  40542  diblsmopel  41617  doch11  41819  recbothd  42431  aks4d1p8d2  42524  aks4d1p8  42526  isprimroot2  42533  posbezout  42539  aks6d1c5lem1  42575  sticksstones1  42585  sticksstones11  42595  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c7  42623  aks5lem8  42640  f1o2d2  42674  dvdsexpnn0  42766  redvmptabs  42792  redivne0bd  42882  prjsprellsp  43044  prjspeclsp  43045  abbibw  43110  istopclsd  43132  eqrabdioph  43209  rexzrexnn0  43232  zindbi  43374  expdiophlem2  43450  onsupeqmax  43674  onsupeqnmax  43675  ordeldif  43686  infordmin  43959  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  sqrtcvallem1  44058  reabsifneg  44059  fsovrfovd  44436  ntrclsiso  44494  ntrneifv3  44509  ntrneineine0lem  44510  ntrneicls11  44517  suprleubrd  44593  suprlubrd  44595  lemuldiv4d  44598  pm14.122a  44849  3impexpbicomi  44908  onfrALTlem5  44969  bitr3VD  45275  onfrALTlem5VD  45311  csbrngVD  45322  pwpwuni  45488  supxrre3  45755  xrralrecnnge  45819  eliooshift  45936  limsupre2lem  46152  liminflimsupclim  46235  xlimbr  46255  smfrec  47217  fsetprcnexALT  47510  f1cof1b  47525  reuf1odnf  47555  2reuimp  47563  ralbinrald  47570  afvco2  47624  dfatdmfcoafv2  47702  recnmulnred  47753  sqrtnegnre  47755  subsubelfzo0  47775  ceilbi  47785  ichcircshi  47914  sprvalpwle2  47949  sprsymrelf1lem  47951  sbcpr  47981  poprelb  47984  31prm  48060  requad01  48097  dfeven3  48134  iseven5  48140  0noddALTV  48165  2noddALTV  48169  fpprmod  48203  sbgoldbaltlem1  48255  bgoldbtbndlem2  48282  dfclnbgr2  48299  dfsclnbgr2  48322  dfvopnbgr2  48329  dfsclnbgr6  48334  isuspgrim0lem  48369  usgrgrtrirex  48426  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgn4cyclex  48602  0nodd  48646  2nodd  48648  isassintop  48686  uzlidlring  48711  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  nn0sumltlt  48826  ply1mulgsumlem2  48863  islindeps  48929  lindslinindsimp1  48933  lindslinindsimp2  48939  snlindsntor  48947  zlmodzxznm  48973  ldepslinc  48985  elbigo2  49028  elbigolo1  49033  logblt1b  49040  fldivexpfllog2  49041  nnolog2flm1  49066  digexp  49083  nn0sumshdiglemB  49096  itsclquadeu  49253  itscnhlinecirc02p  49261  ipolublem  49461  ipoglblem  49464