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  2288  sbal1  2558  euor2  2639  eqabcdv  2895  necon3bbid  2993  necon4bbid  2997  ralanid  3111  rexanid  3112  sbralieALT  3340  ralcom2  3363  rmoanid  3376  reuanid  3377  rabrabi  3431  gencbvex  3507  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  5498  opabid  5499  soeq2  5581  sotrine  5599  posn  5737  xpiindi  5812  dmopab2rex  5899  elpredg  6318  fvopab6  7028  cbvfo  7297  f1eqcocnv  7309  isoid  7337  isoini  7346  isosolem  7355  riotaeqimp  7403  riotarab  7419  resoprab2  7539  tfisi  7870  tfinds2  7875  f1oweALT  7984  dfoprab3  8065  opiota  8070  mpof1o2d  8137  xpord2indlem  8164  xpord3inddlem  8171  mpocurryd  8286  oalimcl  8568  omword  8578  oeword  8599  nnacan  8637  nnmcan  8643  mapsnd  8914  findcard2s  9181  funisfsupp  9359  suppeqfsuppbi  9371  eqinf  9477  inflb  9482  infglb  9483  infglbb  9484  infltoreq  9496  infempty  9501  brwdomn0  9563  cantnfp1lem3  9681  ssrankr1  9847  r1pw  9859  djulf1o  9993  djurf1o  9994  aleph11  10163  alephval3  10189  gch-kn  10762  wunex2  10823  lttri2  11392  wloglei  11848  divne0b  11985  lemul1  12169  nnnle0  12371  div4p1lem1div2  12601  nn0ind-raph  12799  zindd  12800  suprfinzcl  12813  rebtwnz  13074  qreccl  13097  elpq  13103  xrlttri2  13271  2resupmax  13318  xmulneg1  13399  iooshf  13557  difreicc  13615  fzofzim  13844  elfzomelpfzo  13907  elfznelfzo  13908  zmodid2  14039  2submod  14075  modfzo0difsn  14086  om2uzlti  14093  expcan  14312  hashvnfin  14504  hashneq0  14508  prhash2ex  14543  hashgt0elex  14545  hashgt12el  14567  hashgt12el2  14568  hashbclem  14597  hashf1lem2  14601  prprrab  14618  swrd0  14808  pfxn0  14836  swrdswrd  14854  pfxccat3  14883  repswswrd  14935  cshf1  14961  cshw1repsw  14974  relexpindlem  15216  sgnneg  15253  sgn3da  15254  absz  15478  iserex  15824  prodrb  16099  absdvdsb  16444  dvdsabsb  16445  modmulconst  16458  dvdsadd  16472  dvdsabseq  16483  mod2eq0even  16516  oddnn02np1  16518  oddge22np1  16519  evennn02n  16520  evennn2n  16521  zeo5  16526  sadadd2lem2  16620  smupvallem  16653  gcdass  16720  lcmdvds  16783  lcmass  16789  divgcdcoprm0  16840  divgcdcoprmex  16841  1nprm  16854  dvdsnprmd  16865  prmdvdssq  16894  ncoprmlnprm  16904  isevengcd2  16906  m1dvdsndvds  16976  cshws0  17279  sbcie3s  17340  dfiso2  17947  initoid  18176  termoid  18177  funcestrcsetclem8  18321  lublecllem  18532  odudlatb  18699  sgrppropd  18920  issubm2  18999  mgm2nsgrplem2  19118  nsgacs  19372  cycsubg2  19425  gapm  19520  sscntz  19540  pgrpsubgsymgbi  19622  f1omvdcnv  19658  pmtrprfvalrn  19702  odval2  19765  lsmcntz  19893  rngpropd  20396  rnghmf1o  20682  isrngim2  20683  rhmf1o  20727  isrim  20728  df2idl2crng  21577  dfprm2  21779  pzriprnglem10  21796  psgnfix2  21905  islinds3  22140  islindf4  22144  snifpsrbag  22228  gsumply1eq  22627  mdetdiaglem  22913  mdetunilem9  22935  slesolinv  22998  slesolex  23000  cpmatel2  23031  m2cpmghm  23062  m2cpminvid2  23073  pm2mpf1  23117  chfacfscmul0  23176  chfacfscmulfsupp  23177  chfacfpmmul0  23180  chfacfpmmulfsupp  23181  isopn2  23350  cmpsub  23718  connsub  23739  ncvs1  25478  rrxmvallem  25725  itg1mulc  26025  lhop1  26334  mdegleb  26382  lawcos  27144  leibpi  27270  2lgslem1a  27718  2sq2  27760  lestric  28125  bdayons  28662  n0subs2  28750  bdaypw2n0bndlem  28849  angmgmaddov2  29389  colinearalg  29488  edg0iedg0  29633  uhgreq12g  29643  uhgrvtxedgiedgb  29714  usgredg2v  29808  edg0usgr  29834  dfnbgr2  29918  nbuhgr  29924  nbusgredgeu0  29949  nb3grprlem1  29961  nb3grpr  29963  uvtx2vtx1edgb  29980  redwlk  30251  uhgrwkspthlem2  30340  usgr2wlkspth  30345  pthdlem1  30352  cyclnspth  30389  crctcshwlkn0lem1  30399  crctcshwlkn0lem4  30402  crctcsh  30413  iswwlksnx  30429  wwlksm1edg  30470  wwlksnextsurj  30489  wwlksnextproplem3  30500  2wlkdlem4  30517  2wlkdlem5  30518  2pthdlem1  30519  s3wwlks2on  30545  sps3wwlks2on  30546  wpthswwlks2on  30553  elwspths2spth  30559  rusgrnumwwlks  30566  umgrclwwlkge2  30582  clwlkclwwlklem2a4  30588  clwlkclwwlk  30593  clwlkclwwlkflem  30595  clwwisshclwws  30606  isclwwlknx  30627  clwwlknwwlksnb  30646  eclclwwlkn1  30666  clwwlknonel  30686  clwwlknun  30703  3wlkdlem6  30766  frgrncvvdeqlem9  30908  fusgreg2wsp  30937  numclwwlk2lem1lem  30943  extwwlkfab  30953  frgrreggt1  30994  ubthlem1  31472  norm-i  31731  hoeq  32362  nmopgt0  32514  pjimai  32778  chirredi  32996  addltmulALT  33048  opreu2reuALT  33073  sbcies  33084  rmounid  33091  iunrdx  33158  disjrdx  33185  archiabl  33759  islbs5  33935  ist0cld  34465  oms0  34929  eulerpartgbij  35004  reprinrn  35247  usgrgt2cycl  35909  satfv1lem  36127  satf0op  36142  dmopab3rexdif  36170  satefvfmla0  36183  mrsubrn  36278  topfne  37142  unbdqndv1  37374  bj-hbntbi  37606  bj-issetwt  37787  bj-clel3gALT  37963  copsex2d  38060  bj-elid6  38091  dfgcd3  38245  topdifinfeq  38273  wl-sbalnae  38494  sin2h  38533  poimirlem16  38554  poimirlem17  38555  poimirlem25  38563  mbfresfi  38584  itg2addnclem  38589  itg2addnclem2  38590  itg2addnclem3  38591  ftc1anclem1  38611  findcard4  38632  isidlc  38949  eldmressnALTV  39211  islshpsm  40037  lshpkrlem1  40167  opcon1b  40255  lautlt  41148  lauteq  41152  idlaut  41153  diblsmopel  42228  doch11  42430  recbothd  43042  aks4d1p8d2  43135  aks4d1p8  43137  isprimroot2  43144  posbezout  43150  aks6d1c5lem1  43186  sticksstones1  43196  sticksstones11  43206  sticksstones22  43218  aks6d1c6lem3  43222  aks6d1c6lem4  43223  aks6d1c7  43234  aks5lem8  43251  dvdsexpnn0  43386  redvmptabs  43411  redivne0bd  43501  prjsprellsp  43639  prjspeclsp  43640  abbibw  43688  istopclsd  43710  eqrabdioph  43787  rexzrexnn0  43810  zindbi  43952  expdiophlem2  44028  onsupeqmax  44247  onsupeqnmax  44248  ordeldif  44259  infordmin  44532  inintabd  44579  cnvcnvintabd  44599  cnvintabd  44602  sqrtcvallem1  44630  reabsifneg  44631  fsovrfovd  45008  ntrclsiso  45066  ntrneifv3  45081  ntrneineine0lem  45082  ntrneicls11  45089  suprleubrd  45165  suprlubrd  45167  lemuldiv4d  45170  pm14.122a  45405  3impexpbicomi  45463  onfrALTlem5  45524  bitr3VD  45830  onfrALTlem5VD  45866  csbrngVD  45877  pwpwuni  46073  supxrre3  46336  xrralrecnnge  46400  eliooshift  46517  limsupre2lem  46733  liminflimsupclim  46816  xlimbr  46836  smfrec  47798  fsetprcnexALT  48131  f1cof1b  48146  reuf1odnf  48176  2reuimp  48184  ralbinrald  48191  afvco2  48245  dfatdmfcoafv2  48323  recnmulnred  48374  sqrtnegnre  48376  subsubelfzo0  48396  ceilbi  48406  ichcircshi  48535  sprvalpwle2  48570  sprsymrelf1lem  48572  sbcpr  48602  poprelb  48605  31prm  48681  requad01  48718  dfeven3  48755  iseven5  48761  0noddALTV  48786  2noddALTV  48790  fpprmod  48824  sbgoldbaltlem1  48876  bgoldbtbndlem2  48903  dfclnbgr2  48920  dfsclnbgr2  48943  dfvopnbgr2  48950  dfsclnbgr6  48955  isuspgrim0lem  48990  usgrgrtrirex  49047  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  pgn4cyclex  49223  0nodd  49266  2nodd  49268  isassintop  49306  uzlidlring  49331  funcringcsetcALTV2lem8  49393  funcringcsetclem8ALTV  49416  prmringnzring  49433  dfidom2  49439  idomcanl  49443  nn0sumltlt  49461  ply1mulgsumlem2  49498  islindeps  49564  lindslinindsimp1  49568  lindslinindsimp2  49574  snlindsntor  49582  zlmodzxznm  49608  ldepslinc  49620  elbigo2  49663  elbigolo1  49668  logblt1b  49675  fldivexpfllog2  49676  nnolog2flm1  49701  digexp  49718  nn0sumshdiglemB  49731  itsclquadeu  49888  itscnhlinecirc02p  49896  ipolublem  50093  ipoglblem  50096  dvsec  50855  dvcsc  50856  dvcot  50857  ralrals  50903  rexrals  50904  ralals  50909  rexals  50910