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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used 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  546  rbaib  548  baibd  549  anabs5  676  annotanannot  848  pm5.55  963  pm5.54  1035  ninba  1039  pm5.75  1046  sbequ12r  2287  sbal1  2557  euor2  2638  eqabcdv  2894  necon3bbid  2992  necon4bbid  2996  ralanid  3110  rexanid  3111  sbralieALT  3339  ralcom2  3362  rmoanid  3375  reuanid  3376  rabrabi  3430  gencbvex  3506  alexeqg  3605  clel2g  3613  clel3g  3615  clel4g  3617  reurab  3659  reu8  3691  sbceq2a  3751  sbcco2  3766  reu8nf  3824  notabw  4259  2reu4lem  4479  reurexprg  4665  raltpd  4742  ssdifsn  4751  uniprg  4883  disjxun  5101  opabidw  5502  opabid  5503  soeq2  5585  sotrine  5603  posn  5741  xpiindi  5815  dmopab2rex  5901  elpredg  6313  fvopab6  7022  cbvfo  7291  f1eqcocnv  7303  isoid  7331  isoini  7340  isosolem  7349  riotaeqimp  7397  riotarab  7413  resoprab2  7533  tfisi  7856  tfinds2  7861  f1oweALT  7970  dfoprab3  8052  opiota  8057  mpof1o2d  8124  xpord2indlem  8146  xpord3inddlem  8153  mpocurryd  8268  oalimcl  8550  omword  8560  oeword  8581  nnacan  8619  nnmcan  8625  mapsnd  8896  findcard2s  9163  funisfsupp  9340  suppeqfsuppbi  9352  eqinf  9458  inflb  9463  infglb  9464  infglbb  9465  infltoreq  9477  infempty  9482  brwdomn0  9544  cantnfp1lem3  9662  ssrankr1  9820  r1pw  9830  djulf1o  9920  djurf1o  9921  aleph11  10090  alephval3  10116  gch-kn  10689  wunex2  10750  lttri2  11319  wloglei  11773  divne0b  11910  lemul1  12094  nnnle0  12296  div4p1lem1div2  12526  nn0ind-raph  12724  zindd  12725  suprfinzcl  12738  rebtwnz  12999  qreccl  13022  elpq  13028  xrlttri2  13196  2resupmax  13243  xmulneg1  13324  iooshf  13482  difreicc  13540  fzofzim  13768  elfzomelpfzo  13831  elfznelfzo  13832  zmodid2  13963  2submod  13999  modfzo0difsn  14010  om2uzlti  14017  expcan  14236  hashvnfin  14427  hashneq0  14431  prhash2ex  14466  hashgt0elex  14468  hashgt12el  14490  hashgt12el2  14491  hashbclem  14520  hashf1lem2  14524  prprrab  14541  swrd0  14731  pfxn0  14759  swrdswrd  14777  pfxccat3  14806  repswswrd  14858  cshf1  14884  cshw1repsw  14897  relexpindlem  15139  sgnneg  15176  sgn3da  15177  absz  15401  iserex  15747  prodrb  16022  absdvdsb  16367  dvdsabsb  16368  modmulconst  16381  dvdsadd  16395  dvdsabseq  16406  mod2eq0even  16439  oddnn02np1  16441  oddge22np1  16442  evennn02n  16443  evennn2n  16444  zeo5  16449  sadadd2lem2  16543  smupvallem  16576  gcdass  16640  lcmdvds  16701  lcmass  16707  divgcdcoprm0  16758  divgcdcoprmex  16759  1nprm  16772  dvdsnprmd  16783  prmdvdssq  16812  ncoprmlnprm  16822  isevengcd2  16824  m1dvdsndvds  16893  cshws0  17196  sbcie3s  17257  dfiso2  17864  initoid  18093  termoid  18094  funcestrcsetclem8  18238  lublecllem  18449  odudlatb  18616  sgrppropd  18836  issubm2  18915  mgm2nsgrplem2  19034  nsgacs  19288  cycsubg2  19341  gapm  19436  sscntz  19456  pgrpsubgsymgbi  19538  f1omvdcnv  19574  pmtrprfvalrn  19618  odval2  19681  lsmcntz  19809  rngpropd  20312  rnghmf1o  20596  isrngim2  20597  rhmf1o  20641  isrim  20642  df2idl2crng  21487  dfprm2  21689  pzriprnglem10  21706  psgnfix2  21815  islinds3  22050  islindf4  22054  snifpsrbag  22138  gsumply1eq  22537  mdetdiaglem  22823  mdetunilem9  22845  slesolinv  22908  slesolex  22910  cpmatel2  22941  m2cpmghm  22972  m2cpminvid2  22983  pm2mpf1  23027  chfacfscmul0  23086  chfacfscmulfsupp  23087  chfacfpmmul0  23090  chfacfpmmulfsupp  23091  isopn2  23260  cmpsub  23628  connsub  23649  ncvs1  25388  rrxmvallem  25635  itg1mulc  25935  lhop1  26244  mdegleb  26292  lawcos  27056  leibpi  27182  2lgslem1a  27630  2sq2  27672  lestric  28007  bdayons  28544  n0subs2  28632  bdaypw2n0bndlem  28731  angmgmaddov2  29271  colinearalg  29370  edg0iedg0  29515  uhgreq12g  29525  uhgrvtxedgiedgb  29596  usgredg2v  29690  edg0usgr  29716  dfnbgr2  29800  nbuhgr  29806  nbusgredgeu0  29831  nb3grprlem1  29843  nb3grpr  29845  uvtx2vtx1edgb  29862  redwlk  30133  uhgrwkspthlem2  30222  usgr2wlkspth  30227  pthdlem1  30234  cyclnspth  30271  crctcshwlkn0lem1  30281  crctcshwlkn0lem4  30284  crctcsh  30295  iswwlksnx  30311  wwlksm1edg  30352  wwlksnextsurj  30371  wwlksnextproplem3  30382  2wlkdlem4  30399  2wlkdlem5  30400  2pthdlem1  30401  s3wwlks2on  30427  sps3wwlks2on  30428  wpthswwlks2on  30435  elwspths2spth  30441  rusgrnumwwlks  30448  umgrclwwlkge2  30464  clwlkclwwlklem2a4  30470  clwlkclwwlk  30475  clwlkclwwlkflem  30477  clwwisshclwws  30488  isclwwlknx  30509  clwwlknwwlksnb  30528  eclclwwlkn1  30548  clwwlknonel  30568  clwwlknun  30585  3wlkdlem6  30648  frgrncvvdeqlem9  30790  fusgreg2wsp  30819  numclwwlk2lem1lem  30825  extwwlkfab  30835  frgrreggt1  30876  ubthlem1  31354  norm-i  31613  hoeq  32244  nmopgt0  32396  pjimai  32660  chirredi  32878  addltmulALT  32930  opreu2reuALT  32955  sbcies  32966  rmounid  32973  iunrdx  33040  disjrdx  33067  archiabl  33641  islbs5  33816  ist0cld  34346  oms0  34811  eulerpartgbij  34886  reprinrn  35129  usgrgt2cycl  35726  satfv1lem  35944  satf0op  35959  dmopab3rexdif  35987  satefvfmla0  36000  mrsubrn  36095  topfne  36976  unbdqndv1  37208  bj-hbntbi  37440  bj-issetwt  37621  bj-clel3gALT  37795  copsex2d  37894  bj-elid6  37925  dfgcd3  38079  topdifinfeq  38107  wl-sbalnae  38328  sin2h  38367  poimirlem16  38388  poimirlem17  38389  poimirlem25  38397  mbfresfi  38418  itg2addnclem  38423  itg2addnclem2  38424  itg2addnclem3  38425  ftc1anclem1  38445  findcard4  38466  isidlc  38768  eldmressnALTV  39030  islshpsm  39856  lshpkrlem1  39986  opcon1b  40074  lautlt  40967  lauteq  40971  idlaut  40972  diblsmopel  42047  doch11  42249  recbothd  42861  aks4d1p8d2  42954  aks4d1p8  42956  isprimroot2  42963  posbezout  42969  aks6d1c5lem1  43005  sticksstones1  43015  sticksstones11  43025  sticksstones22  43037  aks6d1c6lem3  43041  aks6d1c6lem4  43042  aks6d1c7  43053  aks5lem8  43070  dvdsexpnn0  43212  redvmptabs  43238  redivne0bd  43328  prjsprellsp  43460  prjspeclsp  43461  abbibw  43526  istopclsd  43548  eqrabdioph  43625  rexzrexnn0  43648  zindbi  43790  expdiophlem2  43866  onsupeqmax  44090  onsupeqnmax  44091  ordeldif  44102  infordmin  44375  inintabd  44422  cnvcnvintabd  44443  cnvintabd  44446  sqrtcvallem1  44474  reabsifneg  44475  fsovrfovd  44852  ntrclsiso  44910  ntrneifv3  44925  ntrneineine0lem  44926  ntrneicls11  44933  suprleubrd  45009  suprlubrd  45011  lemuldiv4d  45014  pm14.122a  45249  3impexpbicomi  45307  onfrALTlem5  45368  bitr3VD  45674  onfrALTlem5VD  45710  csbrngVD  45721  pwpwuni  45894  supxrre3  46158  xrralrecnnge  46222  eliooshift  46339  limsupre2lem  46555  liminflimsupclim  46638  xlimbr  46658  smfrec  47620  fsetprcnexALT  47953  f1cof1b  47968  reuf1odnf  47998  2reuimp  48006  ralbinrald  48013  afvco2  48067  dfatdmfcoafv2  48145  recnmulnred  48196  sqrtnegnre  48198  subsubelfzo0  48218  ceilbi  48228  ichcircshi  48357  sprvalpwle2  48392  sprsymrelf1lem  48394  sbcpr  48424  poprelb  48427  31prm  48503  requad01  48540  dfeven3  48577  iseven5  48583  0noddALTV  48608  2noddALTV  48612  fpprmod  48646  sbgoldbaltlem1  48698  bgoldbtbndlem2  48725  dfclnbgr2  48742  dfsclnbgr2  48765  dfvopnbgr2  48772  dfsclnbgr6  48777  isuspgrim0lem  48812  usgrgrtrirex  48869  usgrexmpl2nb1  48951  usgrexmpl2nb2  48952  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem2lem3  49035  pgn4cyclex  49045  0nodd  49088  2nodd  49090  isassintop  49128  uzlidlring  49153  funcringcsetcALTV2lem8  49215  funcringcsetclem8ALTV  49238  prmringnzring  49255  dfidom2  49261  idomcanl  49265  nn0sumltlt  49283  ply1mulgsumlem2  49320  islindeps  49386  lindslinindsimp1  49390  lindslinindsimp2  49396  snlindsntor  49404  zlmodzxznm  49430  ldepslinc  49442  elbigo2  49485  elbigolo1  49490  logblt1b  49497  fldivexpfllog2  49498  nnolog2flm1  49523  digexp  49540  nn0sumshdiglemB  49553  itsclquadeu  49710  itscnhlinecirc02p  49718  ipolublem  49915  ipoglblem  49918  dvsec  50692  dvcsc  50693  dvcot  50694  ralrals  50740  rexrals  50741  ralals  50746  rexals  50747