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  663  annotanannot  834  pm5.55  950  pm5.54  1019  ninba  1023  pm5.75  1030  sbequ12r  2257  sbal1  2530  euor2  2611  eqabcdv  2868  necon3bbid  2967  necon4bbid  2971  ralanid  3082  rexanid  3083  sbralieALT  3321  ralcom2  3345  rmoanid  3358  reuanid  3359  rabrabi  3416  gencbvex  3497  alexeqg  3603  clel2g  3611  clel3g  3613  clel4g  3615  reurab  3657  reu8  3689  sbceq2a  3750  sbcco2  3765  reu8nf  3825  notabw  4263  2reu4lem  4474  reurexprg  4659  raltpd  4736  ssdifsn  4742  uniprg  4877  disjxun  5094  opabidw  5470  opabid  5471  soeq2  5552  sotrine  5570  posn  5708  xpiindi  5782  dmopab2rex  5864  elpredg  6271  fvopab6  6973  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  xpord2indlem  8087  xpord3inddlem  8094  mpocurryd  8209  oalimcl  8485  omword  8495  oeword  8516  nnacan  8554  nnmcan  8560  mapsnd  8822  findcard2s  9088  funisfsupp  9268  suppeqfsuppbi  9280  eqinf  9386  inflb  9391  infglb  9392  infglbb  9393  infltoreq  9405  infempty  9410  brwdomn0  9472  cantnfp1lem3  9587  ssrankr1  9745  r1pw  9755  djulf1o  9822  djurf1o  9823  aleph11  9992  alephval3  10018  gch-kn  10586  wunex2  10647  lttri2  11213  wloglei  11667  divne0b  11805  lemul1  11991  nnnle0  12176  div4p1lem1div2  12394  nn0ind-raph  12590  zindd  12591  suprfinzcl  12604  rebtwnz  12858  qreccl  12880  elpq  12886  xrlttri2  13054  2resupmax  13101  xmulneg1  13182  iooshf  13340  difreicc  13398  fzofzim  13623  elfzomelpfzo  13686  elfznelfzo  13687  zmodid2  13817  2submod  13853  modfzo0difsn  13864  om2uzlti  13871  expcan  14090  hashvnfin  14281  hashneq0  14285  prhash2ex  14320  hashgt0elex  14322  hashgt12el  14343  hashgt12el2  14344  hashbclem  14373  hashf1lem2  14377  prprrab  14394  swrd0  14580  pfxn0  14608  swrdswrd  14626  pfxccat3  14655  repswswrd  14705  cshf1  14731  cshw1repsw  14744  relexpindlem  14984  absz  15232  iserex  15578  prodrb  15853  absdvdsb  16199  dvdsabsb  16200  modmulconst  16213  dvdsadd  16227  dvdsabseq  16238  mod2eq0even  16271  oddnn02np1  16273  oddge22np1  16274  evennn02n  16275  evennn2n  16276  zeo5  16281  sadadd2lem2  16375  smupvallem  16408  gcdass  16472  lcmdvds  16533  lcmass  16539  divgcdcoprm0  16590  divgcdcoprmex  16591  1nprm  16604  dvdsnprmd  16615  prmdvdssq  16643  ncoprmlnprm  16653  isevengcd2  16655  m1dvdsndvds  16724  cshws0  17027  sbcie3s  17087  dfiso2  17694  initoid  17923  termoid  17924  funcestrcsetclem8  18068  lublecllem  18279  odudlatb  18446  sgrppropd  18654  issubm2  18727  mgm2nsgrplem2  18842  nsgacs  19089  cycsubg2  19137  gapm  19233  sscntz  19253  pgrpsubgsymgbi  19335  f1omvdcnv  19371  pmtrprfvalrn  19415  odval2  19478  lsmcntz  19606  rngpropd  20107  rnghmf1o  20386  isrngim2  20387  rhmf1o  20424  isrim  20425  dfprm2  21426  pzriprnglem10  21443  psgnfix2  21552  islinds3  21787  islindf4  21791  snifpsrbag  21874  gsumply1eq  22251  mdetdiaglem  22540  mdetunilem9  22562  slesolinv  22622  slesolex  22624  cpmatel2  22655  m2cpmghm  22686  m2cpminvid2  22697  pm2mpf1  22741  chfacfscmul0  22800  chfacfscmulfsupp  22801  chfacfpmmul0  22804  chfacfpmmulfsupp  22805  isopn2  22974  cmpsub  23342  connsub  23363  ncvs1  25111  rrxmvallem  25358  itg1mulc  25659  lhop1  25973  mdegleb  26023  lawcos  26780  leibpi  26906  2lgslem1a  27356  2sq2  27398  sletric  27730  bdayon  28240  n0subs2  28323  bdaypw2n0s  28420  colinearalg  28932  edg0iedg0  29077  uhgreq12g  29087  uhgrvtxedgiedgb  29158  usgredg2v  29249  edg0usgr  29275  dfnbgr2  29359  nbuhgr  29365  nbusgredgeu0  29390  nb3grprlem1  29402  nb3grpr  29404  uvtx2vtx1edgb  29421  redwlk  29693  uhgrwkspthlem2  29776  usgr2wlkspth  29781  pthdlem1  29788  cyclnspth  29823  crctcshwlkn0lem1  29832  crctcshwlkn0lem4  29835  crctcsh  29846  iswwlksnx  29862  wwlksm1edg  29903  wwlksnextsurj  29922  wwlksnextproplem3  29933  2wlkdlem4  29950  2wlkdlem5  29951  2pthdlem1  29952  s3wwlks2on  29978  sps3wwlks2on  29979  wpthswwlks2on  29986  elwspths2spth  29992  rusgrnumwwlks  29999  umgrclwwlkge2  30015  clwlkclwwlklem2a4  30021  clwlkclwwlk  30026  clwlkclwwlkflem  30028  clwwisshclwws  30039  isclwwlknx  30060  clwwlknwwlksnb  30079  eclclwwlkn1  30099  clwwlknonel  30119  clwwlknun  30136  3wlkdlem6  30189  frgrncvvdeqlem9  30331  fusgreg2wsp  30360  numclwwlk2lem1lem  30366  extwwlkfab  30376  frgrreggt1  30417  ubthlem1  30894  norm-i  31153  hoeq  31784  nmopgt0  31936  pjimai  32200  chirredi  32418  addltmulALT  32470  bian1d  32479  opreu2reuALT  32500  sbcies  32511  rmounid  32518  iunrdx  32587  disjrdx  32615  sgnneg  32863  sgn3da  32864  archiabl  33229  islbs5  33410  ist0cld  33939  oms0  34403  eulerpartgbij  34478  reprinrn  34724  usgrgt2cycl  35273  satfv1lem  35505  satf0op  35520  dmopab3rexdif  35548  satefvfmla0  35561  mrsubrn  35656  topfne  36497  unbdqndv1  36651  bj-hbntbi  36848  bj-issetwt  37019  bj-clel3gALT  37192  copsex2d  37283  bj-elid6  37314  dfgcd3  37468  topdifinfeq  37494  wl-sbalnae  37706  sin2h  37750  poimirlem16  37776  poimirlem17  37777  poimirlem25  37785  mbfresfi  37806  itg2addnclem  37811  itg2addnclem2  37812  itg2addnclem3  37813  ftc1anclem1  37833  isidlc  38155  eldmressnALTV  38411  islshpsm  39179  lshpkrlem1  39309  opcon1b  39397  lautlt  40290  lauteq  40294  idlaut  40295  diblsmopel  41370  doch11  41572  recbothd  42185  aks4d1p8d2  42278  aks4d1p8  42280  isprimroot2  42287  posbezout  42293  aks6d1c5lem1  42329  sticksstones1  42339  sticksstones11  42349  sticksstones22  42361  aks6d1c6lem3  42365  aks6d1c6lem4  42366  aks6d1c7  42377  aks5lem8  42394  f1o2d2  42431  dvdsexpnn0  42531  redvmptabs  42557  prjsprellsp  42796  prjspeclsp  42797  abbibw  42862  istopclsd  42884  eqrabdioph  42961  rexzrexnn0  42988  zindbi  43130  expdiophlem2  43206  onsupeqmax  43430  onsupeqnmax  43431  ordeldif  43442  infordmin  43715  inintabd  43762  cnvcnvintabd  43783  cnvintabd  43786  sqrtcvallem1  43814  reabsifneg  43815  fsovrfovd  44192  ntrclsiso  44250  ntrneifv3  44265  ntrneineine0lem  44266  ntrneicls11  44273  suprleubrd  44349  suprlubrd  44351  lemuldiv4d  44354  pm14.122a  44605  3impexpbicomi  44664  onfrALTlem5  44725  bitr3VD  45031  onfrALTlem5VD  45067  csbrngVD  45078  pwpwuni  45244  supxrre3  45512  xrralrecnnge  45576  eliooshift  45694  limsupre2lem  45910  liminflimsupclim  45993  xlimbr  46013  smfrec  46975  fsetprcnexALT  47250  f1cof1b  47265  reuf1odnf  47295  2reuimp  47303  ralbinrald  47310  afvco2  47364  dfatdmfcoafv2  47442  recnmulnred  47493  sqrtnegnre  47495  subsubelfzo0  47514  ceilbi  47521  ichcircshi  47642  sprvalpwle2  47677  sprsymrelf1lem  47679  sbcpr  47709  poprelb  47712  31prm  47785  requad01  47809  dfeven3  47846  iseven5  47852  0noddALTV  47877  2noddALTV  47881  fpprmod  47915  sbgoldbaltlem1  47967  bgoldbtbndlem2  47994  dfclnbgr2  48011  dfsclnbgr2  48034  dfvopnbgr2  48041  dfsclnbgr6  48046  isuspgrim0lem  48081  usgrgrtrirex  48138  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgn4cyclex  48314  0nodd  48358  2nodd  48360  isassintop  48398  uzlidlring  48423  funcringcsetcALTV2lem8  48485  funcringcsetclem8ALTV  48508  nn0sumltlt  48538  ply1mulgsumlem2  48575  islindeps  48641  lindslinindsimp1  48645  lindslinindsimp2  48651  snlindsntor  48659  zlmodzxznm  48685  ldepslinc  48697  elbigo2  48740  elbigolo1  48745  logblt1b  48752  fldivexpfllog2  48753  nnolog2flm1  48778  digexp  48795  nn0sumshdiglemB  48808  itsclquadeu  48965  itscnhlinecirc02p  48973  ipolublem  49173  ipoglblem  49176