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  662  annotanannot  834  pm5.55  949  pm5.54  1018  ninba  1022  pm5.75  1029  sbequ12r  2253  sbal1  2536  euor2  2616  eqabcdv  2879  necon3bbid  2984  necon4bbid  2988  ralanid  3101  rexanid  3102  sbralieALT  3367  ralcom2  3385  rmoanid  3398  reuanid  3399  rabrabi  3463  gencbvex  3553  sbhypfOLD  3557  alexeqg  3664  clel2g  3672  clel3g  3674  clel4g  3676  reurab  3723  reu8  3755  sbceq2a  3816  sbcco2  3831  reu8nf  3899  notabw  4332  2reu4lem  4545  reurexprg  4729  raltpd  4806  ssdifsn  4813  uniprg  4947  disjxun  5164  opabidw  5543  opabid  5544  soeq2  5630  sotrine  5647  posn  5785  xpiindi  5860  dmopab2rex  5942  elpredg  6346  fvopab6  7063  cbvfo  7325  f1eqcocnv  7337  isoid  7365  isoini  7374  isosolem  7383  riotaeqimp  7431  riotarab  7447  resoprab2  7569  tfisi  7896  tfinds2  7901  f1oweALT  8013  dfoprab3  8095  opiota  8100  xpord2indlem  8188  xpord3inddlem  8195  mpocurryd  8310  oalimcl  8616  omword  8626  oeword  8646  nnacan  8684  nnmcan  8690  mapsnd  8944  findcard2s  9231  funisfsupp  9437  suppeqfsuppbi  9448  eqinf  9553  inflb  9558  infglb  9559  infglbb  9560  infltoreq  9571  infempty  9576  brwdomn0  9638  cantnfp1lem3  9749  ssrankr1  9904  r1pw  9914  djulf1o  9981  djurf1o  9982  aleph11  10153  alephval3  10179  gch-kn  10746  wunex2  10807  lttri2  11372  wloglei  11822  divne0b  11960  lemul1  12146  nnnle0  12326  div4p1lem1div2  12548  nn0ind-raph  12743  zindd  12744  suprfinzcl  12757  rebtwnz  13012  qreccl  13034  elpq  13040  xrlttri2  13204  2resupmax  13250  xmulneg1  13331  iooshf  13486  difreicc  13544  fzofzim  13763  elfzomelpfzo  13821  elfznelfzo  13822  zmodid2  13950  2submod  13983  modfzo0difsn  13994  om2uzlti  14001  expcan  14219  hashvnfin  14409  hashneq0  14413  prhash2ex  14448  hashgt0elex  14450  hashgt12el  14471  hashgt12el2  14472  hashbclem  14501  hashf1lem2  14505  prprrab  14522  swrd0  14706  pfxn0  14734  swrdswrd  14753  pfxccat3  14782  repswswrd  14832  cshf1  14858  cshw1repsw  14871  relexpindlem  15112  absz  15360  iserex  15705  prodrb  15980  absdvdsb  16323  dvdsabsb  16324  modmulconst  16336  dvdsadd  16350  dvdsabseq  16361  mod2eq0even  16394  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  zeo5  16404  sadadd2lem2  16496  smupvallem  16529  gcdass  16594  lcmdvds  16655  lcmass  16661  divgcdcoprm0  16712  divgcdcoprmex  16713  1nprm  16726  dvdsnprmd  16737  prmdvdssq  16765  ncoprmlnprm  16775  isevengcd2  16777  m1dvdsndvds  16845  cshws0  17149  sbcie3s  17209  dfiso2  17833  initoid  18068  termoid  18069  funcestrcsetclem8  18216  lublecllem  18430  odudlatb  18595  sgrppropd  18769  issubm2  18839  mgm2nsgrplem2  18954  nsgacs  19202  cycsubg2  19250  gapm  19346  sscntz  19366  pgrpsubgsymgbi  19450  f1omvdcnv  19486  pmtrprfvalrn  19530  odval2  19593  lsmcntz  19721  rngpropd  20201  rnghmf1o  20478  isrngim2  20479  rhmf1o  20517  isrim  20518  isrimOLD  20519  dfprm2  21507  pzriprnglem10  21524  psgnfix2  21640  islinds3  21877  islindf4  21881  snifpsrbag  21963  gsumply1eq  22334  mdetdiaglem  22625  mdetunilem9  22647  slesolinv  22707  slesolex  22709  cpmatel2  22740  m2cpmghm  22771  m2cpminvid2  22782  pm2mpf1  22826  chfacfscmul0  22885  chfacfscmulfsupp  22886  chfacfpmmul0  22889  chfacfpmmulfsupp  22890  isopn2  23061  cmpsub  23429  connsub  23450  ncvs1  25210  rrxmvallem  25457  itg1mulc  25759  lhop1  26073  mdegleb  26123  lawcos  26877  leibpi  27003  2lgslem1a  27453  2sq2  27495  sletric  27827  0reno  28447  colinearalg  28943  edg0iedg0  29090  uhgreq12g  29100  uhgrvtxedgiedgb  29171  usgredg2v  29262  edg0usgr  29288  dfnbgr2  29372  nbuhgr  29378  nbusgredgeu0  29403  nb3grprlem1  29415  nb3grpr  29417  uvtx2vtx1edgb  29434  redwlk  29708  uhgrwkspthlem2  29790  usgr2wlkspth  29795  pthdlem1  29802  cyclnspth  29836  crctcshwlkn0lem1  29843  crctcshwlkn0lem4  29846  crctcsh  29857  iswwlksnx  29873  wwlksm1edg  29914  wwlksnextsurj  29933  wwlksnextproplem3  29944  2wlkdlem4  29961  2wlkdlem5  29962  2pthdlem1  29963  s3wwlks2on  29989  wpthswwlks2on  29994  elwspths2spth  30000  rusgrnumwwlks  30007  umgrclwwlkge2  30023  clwlkclwwlklem2a4  30029  clwlkclwwlk  30034  clwlkclwwlkflem  30036  clwwisshclwws  30047  isclwwlknx  30068  clwwlknwwlksnb  30087  eclclwwlkn1  30107  clwwlknonel  30127  clwwlknun  30144  3wlkdlem6  30197  frgrncvvdeqlem9  30339  fusgreg2wsp  30368  numclwwlk2lem1lem  30374  extwwlkfab  30384  frgrreggt1  30425  ubthlem1  30902  norm-i  31161  hoeq  31792  nmopgt0  31944  pjimai  32208  chirredi  32426  addltmulALT  32478  bian1d  32484  opreu2reuALT  32505  sbcies  32516  rmounid  32523  iunrdx  32586  disjrdx  32613  cnvoprabOLD  32734  archiabl  33178  islbs5  33373  ist0cld  33779  oms0  34262  eulerpartgbij  34337  sgnneg  34505  sgn3da  34506  reprinrn  34595  usgrgt2cycl  35098  satfv1lem  35330  satf0op  35345  dmopab3rexdif  35373  satefvfmla0  35386  mrsubrn  35481  topfne  36320  unbdqndv1  36474  bj-hbntbi  36670  bj-issetwt  36841  bj-clel3gALT  37014  copsex2d  37105  bj-elid6  37136  dfgcd3  37290  topdifinfeq  37316  wl-sbalnae  37516  sin2h  37570  poimirlem16  37596  poimirlem17  37597  poimirlem25  37605  mbfresfi  37626  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  ftc1anclem1  37653  isidlc  37975  eldmressnALTV  38228  islshpsm  38936  lshpkrlem1  39066  opcon1b  39154  lautlt  40048  lauteq  40052  idlaut  40053  diblsmopel  41128  doch11  41330  recbothd  41949  aks4d1p8d2  42042  aks4d1p8  42044  isprimroot2  42051  posbezout  42057  aks6d1c5lem1  42093  sticksstones1  42103  sticksstones11  42113  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c7  42141  aks5lem8  42158  metakunt16  42177  f1o2d2  42228  dvdsexpnn0  42321  prjsprellsp  42566  prjspeclsp  42567  abbibw  42632  istopclsd  42656  eqrabdioph  42733  rexzrexnn0  42760  zindbi  42903  expdiophlem2  42979  onsupeqmax  43207  onsupeqnmax  43208  ordeldif  43220  infordmin  43494  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  sqrtcvallem1  43593  reabsifneg  43594  fsovrfovd  43971  ntrclsiso  44029  ntrneifv3  44044  ntrneineine0lem  44045  ntrneicls11  44052  suprleubrd  44128  suprlubrd  44130  lemuldiv4d  44133  pm14.122a  44391  3impexpbicomi  44451  onfrALTlem5  44513  bitr3VD  44820  onfrALTlem5VD  44856  csbrngVD  44867  pwpwuni  44959  supxrre3  45240  xrralrecnnge  45305  eliooshift  45424  limsupre2lem  45645  liminflimsupclim  45728  xlimbr  45748  smfrec  46710  fsetprcnexALT  46977  f1cof1b  46992  reuf1odnf  47022  2reuimp  47030  ralbinrald  47037  afvco2  47091  dfatdmfcoafv2  47169  recnmulnred  47220  sqrtnegnre  47222  subsubelfzo0  47241  ichcircshi  47328  sprvalpwle2  47363  sprsymrelf1lem  47365  sbcpr  47395  poprelb  47398  31prm  47471  requad01  47495  dfeven3  47532  iseven5  47538  0noddALTV  47563  2noddALTV  47567  fpprmod  47601  sbgoldbaltlem1  47653  bgoldbtbndlem2  47680  dfclnbgr2  47697  dfsclnbgr2  47718  dfvopnbgr2  47725  dfsclnbgr6  47730  isuspgrim0lem  47755  usgrgrtrirex  47799  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  0nodd  47893  2nodd  47895  isassintop  47933  uzlidlring  47958  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  nn0sumltlt  48075  ply1mulgsumlem2  48116  islindeps  48182  lindslinindsimp1  48186  lindslinindsimp2  48192  snlindsntor  48200  zlmodzxznm  48226  ldepslinc  48238  difmodm1lt  48256  elbigo2  48286  elbigolo1  48291  logblt1b  48298  fldivexpfllog2  48299  nnolog2flm1  48324  digexp  48341  nn0sumshdiglemB  48354  itsclquadeu  48511  itscnhlinecirc02p  48519  ipolublem  48658  ipoglblem  48661