Theorem bicomd 224

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  impbid2  227  imbitrrid  247  ibir  269  bitr2d  281  bitr3d  282  bitr4d  283  bitr2id  285  bitr2di  289  con1bid  356  pm5.5  362  imnot  366  baibr  541  rbaib  543  baibd  544  anabs5  669  annotanannot  840  pm5.55  956  pm5.54  1025  ninba  1029  pm5.75  1036  sbequ12r  2264  sbal1  2536  euor2  2617  eqabcdv  2873  necon3bbid  2971  necon4bbid  2975  ralanid  3087  rexanid  3088  sbralieALT  3318  ralcom2  3341  rmoanid  3354  reuanid  3355  rabrabi  3410  gencbvex  3488  alexeqg  3589  clel2g  3597  clel3g  3599  clel4g  3601  reurab  3642  reu8  3674  sbceq2a  3735  sbcco2  3750  reu8nf  3809  notabw  4241  2reu4lem  4451  reurexprg  4636  raltpd  4713  ssdifsn  4721  uniprg  4854  disjxun  5070  opabidw  5466  opabid  5467  soeq2  5548  sotrine  5566  posn  5704  xpiindi  5777  dmopab2rex  5859  elpredg  6266  fvopab6  6970  cbvfo  7233  f1eqcocnv  7245  isoid  7273  isoini  7282  isosolem  7291  riotaeqimp  7339  riotarab  7355  resoprab2  7475  tfisi  7799  tfinds2  7804  f1oweALT  7914  dfoprab3  7996  opiota  8001  mpof1o2d  8065  xpord2indlem  8087  xpord3inddlem  8094  mpocurryd  8209  oalimcl  8485  omword  8495  oeword  8516  nnacan  8554  nnmcan  8560  mapsnd  8824  findcard2s  9090  funisfsupp  9270  suppeqfsuppbi  9282  eqinf  9388  inflb  9393  infglb  9394  infglbb  9395  infltoreq  9407  infempty  9412  brwdomn0  9474  cantnfp1lem3  9592  ssrankr1  9750  r1pw  9760  djulf1o  9827  djurf1o  9828  aleph11  9997  alephval3  10023  gch-kn  10591  wunex2  10652  lttri2  11219  wloglei  11673  divne0b  11811  lemul1  11998  nnnle0  12201  div4p1lem1div2  12423  nn0ind-raph  12620  zindd  12621  suprfinzcl  12634  rebtwnz  12888  qreccl  12910  elpq  12916  xrlttri2  13084  2resupmax  13131  xmulneg1  13212  iooshf  13370  difreicc  13428  fzofzim  13655  elfzomelpfzo  13718  elfznelfzo  13719  zmodid2  13849  2submod  13885  modfzo0difsn  13896  om2uzlti  13903  expcan  14122  hashvnfin  14313  hashneq0  14317  prhash2ex  14352  hashgt0elex  14354  hashgt12el  14375  hashgt12el2  14376  hashbclem  14405  hashf1lem2  14409  prprrab  14426  swrd0  14612  pfxn0  14640  swrdswrd  14658  pfxccat3  14687  repswswrd  14737  cshf1  14763  cshw1repsw  14776  relexpindlem  15016  absz  15264  iserex  15610  prodrb  15888  absdvdsb  16234  dvdsabsb  16235  modmulconst  16248  dvdsadd  16262  dvdsabseq  16273  mod2eq0even  16306  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  zeo5  16316  sadadd2lem2  16410  smupvallem  16443  gcdass  16507  lcmdvds  16568  lcmass  16574  divgcdcoprm0  16625  divgcdcoprmex  16626  1nprm  16639  dvdsnprmd  16650  prmdvdssq  16679  ncoprmlnprm  16689  isevengcd2  16691  m1dvdsndvds  16760  cshws0  17063  sbcie3s  17123  dfiso2  17730  initoid  17959  termoid  17960  funcestrcsetclem8  18104  lublecllem  18315  odudlatb  18482  sgrppropd  18690  issubm2  18763  mgm2nsgrplem2  18881  nsgacs  19128  cycsubg2  19176  gapm  19272  sscntz  19292  pgrpsubgsymgbi  19374  f1omvdcnv  19410  pmtrprfvalrn  19454  odval2  19517  lsmcntz  19645  rngpropd  20146  rnghmf1o  20423  isrngim2  20424  rhmf1o  20462  isrim  20463  dfprm2  21448  pzriprnglem10  21465  psgnfix2  21574  islinds3  21809  islindf4  21813  snifpsrbag  21895  gsumply1eq  22295  mdetdiaglem  22581  mdetunilem9  22603  slesolinv  22663  slesolex  22665  cpmatel2  22696  m2cpmghm  22727  m2cpminvid2  22738  pm2mpf1  22782  chfacfscmul0  22841  chfacfscmulfsupp  22842  chfacfpmmul0  22845  chfacfpmmulfsupp  22846  isopn2  23015  cmpsub  23383  connsub  23404  ncvs1  25142  rrxmvallem  25389  itg1mulc  25689  lhop1  25999  mdegleb  26047  lawcos  26798  leibpi  26924  2lgslem1a  27372  2sq2  27414  lestric  27750  bdayons  28286  n0subs2  28374  bdaypw2n0bndlem  28473  colinearalg  28997  edg0iedg0  29142  uhgreq12g  29152  uhgrvtxedgiedgb  29223  usgredg2v  29314  edg0usgr  29340  dfnbgr2  29424  nbuhgr  29430  nbusgredgeu0  29455  nb3grprlem1  29467  nb3grpr  29469  uvtx2vtx1edgb  29486  redwlk  29757  uhgrwkspthlem2  29840  usgr2wlkspth  29845  pthdlem1  29852  cyclnspth  29887  crctcshwlkn0lem1  29896  crctcshwlkn0lem4  29899  crctcsh  29910  iswwlksnx  29926  wwlksm1edg  29967  wwlksnextsurj  29986  wwlksnextproplem3  29997  2wlkdlem4  30014  2wlkdlem5  30015  2pthdlem1  30016  s3wwlks2on  30042  sps3wwlks2on  30043  wpthswwlks2on  30050  elwspths2spth  30056  rusgrnumwwlks  30063  umgrclwwlkge2  30079  clwlkclwwlklem2a4  30085  clwlkclwwlk  30090  clwlkclwwlkflem  30092  clwwisshclwws  30103  isclwwlknx  30124  clwwlknwwlksnb  30143  eclclwwlkn1  30163  clwwlknonel  30183  clwwlknun  30200  3wlkdlem6  30253  frgrncvvdeqlem9  30395  fusgreg2wsp  30424  numclwwlk2lem1lem  30430  extwwlkfab  30440  frgrreggt1  30481  ubthlem1  30959  norm-i  31218  hoeq  31849  nmopgt0  32001  pjimai  32265  chirredi  32483  addltmulALT  32535  opreu2reuALT  32564  sbcies  32575  rmounid  32582  iunrdx  32652  disjrdx  32680  sgnneg  32925  sgn3da  32926  archiabl  33279  islbs5  33463  ist0cld  34017  oms0  34481  eulerpartgbij  34556  reprinrn  34802  usgrgt2cycl  35358  satfv1lem  35590  satf0op  35605  dmopab3rexdif  35633  satefvfmla0  35646  mrsubrn  35741  topfne  36582  unbdqndv1  36814  bj-hbntbi  37047  bj-issetwt  37228  bj-clel3gALT  37401  copsex2d  37499  bj-elid6  37530  dfgcd3  37684  topdifinfeq  37712  wl-sbalnae  37933  sin2h  37977  poimirlem16  38003  poimirlem17  38004  poimirlem25  38012  mbfresfi  38033  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  ftc1anclem1  38060  isidlc  38382  eldmressnALTV  38646  islshpsm  39472  lshpkrlem1  39602  opcon1b  39690  lautlt  40583  lauteq  40587  idlaut  40588  diblsmopel  41663  doch11  41865  recbothd  42477  aks4d1p8d2  42570  aks4d1p8  42572  isprimroot2  42579  posbezout  42585  aks6d1c5lem1  42621  sticksstones1  42631  sticksstones11  42641  sticksstones22  42653  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c7  42669  aks5lem8  42686  dvdsexpnn0  42811  redvmptabs  42837  redivne0bd  42927  prjsprellsp  43061  prjspeclsp  43062  abbibw  43127  istopclsd  43149  eqrabdioph  43226  rexzrexnn0  43249  zindbi  43391  expdiophlem2  43467  onsupeqmax  43691  onsupeqnmax  43692  ordeldif  43703  infordmin  43976  inintabd  44023  cnvcnvintabd  44044  cnvintabd  44047  sqrtcvallem1  44075  reabsifneg  44076  fsovrfovd  44453  ntrclsiso  44511  ntrneifv3  44526  ntrneineine0lem  44527  ntrneicls11  44534  suprleubrd  44610  suprlubrd  44612  lemuldiv4d  44615  pm14.122a  44866  3impexpbicomi  44925  onfrALTlem5  44986  bitr3VD  45292  onfrALTlem5VD  45328  csbrngVD  45339  pwpwuni  45505  supxrre3  45770  xrralrecnnge  45834  eliooshift  45951  limsupre2lem  46167  liminflimsupclim  46250  xlimbr  46270  smfrec  47232  fsetprcnexALT  47525  f1cof1b  47540  reuf1odnf  47570  2reuimp  47578  ralbinrald  47585  afvco2  47639  dfatdmfcoafv2  47717  recnmulnred  47768  sqrtnegnre  47770  subsubelfzo0  47790  ceilbi  47800  ichcircshi  47929  sprvalpwle2  47964  sprsymrelf1lem  47966  sbcpr  47996  poprelb  47999  31prm  48075  requad01  48112  dfeven3  48149  iseven5  48155  0noddALTV  48180  2noddALTV  48184  fpprmod  48218  sbgoldbaltlem1  48270  bgoldbtbndlem2  48297  dfclnbgr2  48314  dfsclnbgr2  48337  dfvopnbgr2  48344  dfsclnbgr6  48349  isuspgrim0lem  48384  usgrgrtrirex  48441  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgn4cyclex  48617  0nodd  48661  2nodd  48663  isassintop  48701  uzlidlring  48726  funcringcsetcALTV2lem8  48788  funcringcsetclem8ALTV  48811  nn0sumltlt  48841  ply1mulgsumlem2  48878  islindeps  48944  lindslinindsimp1  48948  lindslinindsimp2  48954  snlindsntor  48962  zlmodzxznm  48988  ldepslinc  49000  elbigo2  49043  elbigolo1  49048  logblt1b  49055  fldivexpfllog2  49056  nnolog2flm1  49081  digexp  49098  nn0sumshdiglemB  49111  itsclquadeu  49268  itscnhlinecirc02p  49276  ipolublem  49476  ipoglblem  49479