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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  impbid2  229  syl5ibr  249  ibir  271  bitr2d  283  bitr3d  284  bitr4d  285  bitr2id  287  bitr2di  291  con1bid  359  pm5.5  365  imnot  369  baibr  540  rbaib  542  baibd  543  anabs5  663  annotanannot  835  pm5.55  949  pm5.54  1018  ninba  1022  pm5.75  1029  norassOLD  1540  sbequ12r  2252  sbal1  2532  euor2  2614  abbi1dv  2868  necon3bbid  2969  necon4bbid  2973  ralanid  3081  rexanid  3165  ralcom2  3265  sbralie  3371  rabrabi  3393  rabeqcda  3395  gencbvex  3454  sbhypf  3457  alexeqg  3548  clel2g  3556  clel2gOLD  3557  clel3g  3559  clel4g  3561  reu8  3635  sbceq2a  3695  sbcco2  3710  reu8nf  3776  notabw  4204  2reu4lem  4423  reurexprg  4606  raltpd  4683  ssdifsn  4687  uniprg  4822  disjxun  5037  opabidw  5391  opabid  5392  soeq2  5475  posn  5619  xpiindi  5689  dmopab2rex  5771  fvopab6  6829  cbvfo  7077  f1eqcocnv  7089  f1eqcocnvOLD  7090  isoid  7116  isoini  7125  isosolem  7134  riotaeqimp  7175  resoprab2  7307  tfisi  7615  tfinds2  7620  f1oweALT  7723  dfoprab3  7802  opiota  7807  mpocurryd  7989  oalimcl  8266  omword  8276  oeword  8296  nnacan  8334  nnmcan  8340  mapsnd  8545  findcard2s  8821  funisfsupp  8968  suppeqfsuppbi  8977  eqinf  9078  inflb  9083  infglb  9084  infglbb  9085  infltoreq  9096  infempty  9101  brwdomn0  9163  cantnfp1lem3  9273  ssrankr1  9416  r1pw  9426  djulf1o  9493  djurf1o  9494  aleph11  9663  alephval3  9689  gch-kn  10256  wunex2  10317  lttri2  10880  wloglei  11329  divne0b  11466  lemul1  11649  nnnle0  11828  div4p1lem1div2  12050  nn0ind-raph  12242  zindd  12243  suprfinzcl  12257  rebtwnz  12508  qreccl  12530  elpq  12536  xrlttri2  12697  2resupmax  12743  xmulneg1  12824  iooshf  12979  difreicc  13037  fzofzim  13254  elfzomelpfzo  13311  elfznelfzo  13312  zmodid2  13437  2submod  13470  modfzo0difsn  13481  om2uzlti  13488  expcan  13704  hashvnfin  13892  hashneq0  13896  prhash2ex  13931  hashgt0elex  13933  hashgt12el  13954  hashgt12el2  13955  hashbclem  13981  hashf1lem2  13987  prprrab  14004  swrd0  14188  pfxn0  14216  swrdswrd  14235  pfxccat3  14264  repswswrd  14314  cshf1  14340  cshw1repsw  14353  relexpindlem  14591  absz  14840  iserex  15185  prodrb  15457  absdvdsb  15799  dvdsabsb  15800  modmulconst  15812  dvdsadd  15826  dvdsabseq  15837  mod2eq0even  15870  oddnn02np1  15872  oddge22np1  15873  evennn02n  15874  evennn2n  15875  zeo5  15880  sadadd2lem2  15972  smupvallem  16005  gcdass  16070  lcmdvds  16128  lcmass  16134  divgcdcoprm0  16185  divgcdcoprmex  16186  1nprm  16199  dvdsnprmd  16210  prmdvdssq  16238  ncoprmlnprm  16247  isevengcd2  16249  m1dvdsndvds  16314  cshws0  16618  sbcie2s  16721  sbcie3s  16722  dfiso2  17231  initoid  17461  termoid  17462  funcestrcsetclem8  17608  lublecllem  17820  odudlatb  17985  issubm2  18185  mgm2nsgrplem2  18300  nsgacs  18532  cycsubg2  18571  gapm  18654  sscntz  18674  pgrpsubgsymgbi  18754  f1omvdcnv  18790  pmtrprfvalrn  18834  odval2  18897  lsmcntz  19023  rhmf1o  19706  isrim  19707  dfprm2  20414  psgnfix2  20515  islinds3  20750  islindf4  20754  snifpsrbag  20835  gsumply1eq  21180  mdetdiaglem  21449  mdetunilem9  21471  slesolinv  21531  slesolex  21533  cpmatel2  21564  m2cpmghm  21595  m2cpminvid2  21606  pm2mpf1  21650  chfacfscmul0  21709  chfacfscmulfsupp  21710  chfacfpmmul0  21713  chfacfpmmulfsupp  21714  isopn2  21883  cmpsub  22251  connsub  22272  ncvs1  24008  rrxmvallem  24255  itg1mulc  24556  lhop1  24865  mdegleb  24916  lawcos  25653  leibpi  25779  2lgslem1a  26226  2sq2  26268  iscgra  26854  colinearalg  26955  edg0iedg0  27100  uhgreq12g  27110  uhgrvtxedgiedgb  27181  usgredg2v  27269  edg0usgr  27295  dfnbgr2  27379  nbuhgr  27385  nbusgredgeu0  27410  nb3grprlem1  27422  nb3grpr  27424  uvtx2vtx1edgb  27441  redwlk  27714  uhgrwkspthlem2  27795  usgr2wlkspth  27800  pthdlem1  27807  cyclnspth  27841  crctcshwlkn0lem1  27848  crctcshwlkn0lem4  27851  crctcsh  27862  iswwlksnx  27878  wwlksm1edg  27919  wwlksnextsurj  27938  wwlksnextproplem3  27949  2wlkdlem4  27966  2wlkdlem5  27967  2pthdlem1  27968  s3wwlks2on  27994  wpthswwlks2on  27999  elwspths2spth  28005  rusgrnumwwlks  28012  umgrclwwlkge2  28028  clwlkclwwlklem2a4  28034  clwlkclwwlk  28039  clwlkclwwlkflem  28041  clwwisshclwws  28052  isclwwlknx  28073  clwwlknwwlksnb  28092  eclclwwlkn1  28112  clwwlknonel  28132  clwwlknun  28149  3wlkdlem6  28202  frgrncvvdeqlem9  28344  fusgreg2wsp  28373  numclwwlk2lem1lem  28379  extwwlkfab  28389  frgrreggt1  28430  ubthlem1  28905  norm-i  29164  hoeq  29795  nmopgt0  29947  pjimai  30211  chirredi  30429  addltmulALT  30481  opreu2reuALT  30498  sbcies  30509  rmounid  30516  iunrdx  30576  disjrdx  30603  cnvoprabOLD  30729  archiabl  31125  ist0cld  31451  oms0  31930  eulerpartgbij  32005  sgnneg  32173  sgn3da  32174  reprinrn  32264  usgrgt2cycl  32759  satfv1lem  32991  satf0op  33006  dmopab3rexdif  33034  satefvfmla0  33047  mrsubrn  33142  riotarab  33342  reurab  33343  sotrine  33404  xpord2ind  33474  xpord3ind  33480  topfne  34229  unbdqndv1  34374  bj-hbntbi  34572  bj-issetwt  34745  bj-clel3gALT  34907  copsex2d  34994  bj-elid6  35025  dfgcd3  35178  topdifinfeq  35207  wl-sb6rft  35389  wl-sbalnae  35403  sin2h  35453  poimirlem16  35479  poimirlem17  35480  poimirlem25  35488  mbfresfi  35509  itg2addnclem  35514  itg2addnclem2  35515  itg2addnclem3  35516  ftc1anclem1  35536  isidlc  35859  islshpsm  36680  lshpkrlem1  36810  opcon1b  36898  lautlt  37791  lauteq  37795  idlaut  37796  diblsmopel  38871  doch11  39073  recbothd  39684  sticksstones1  39771  sticksstones11  39781  metakunt16  39803  dvdsexpnn0  39990  prjsprellsp  40099  prjspeclsp  40100  istopclsd  40166  eqrabdioph  40243  rexzrexnn0  40270  zindbi  40412  expdiophlem2  40488  infordmin  40765  inintabd  40804  cnvcnvintabd  40825  cnvintabd  40828  sqrtcvallem1  40856  reabsifneg  40857  fsovrfovd  41235  ntrclsiso  41295  ntrneifv3  41310  ntrneineine0lem  41311  ntrneicls11  41318  suprleubrd  41395  suprlubrd  41397  lemuldiv4d  41400  pm14.122a  41654  3impexpbicomi  41714  onfrALTlem5  41776  bitr3VD  42083  onfrALTlem5VD  42119  csbrngVD  42130  pwpwuni  42219  supxrre3  42478  xrralrecnnge  42544  eliooshift  42660  limsupre2lem  42883  liminflimsupclim  42966  xlimbr  42986  smfrec  43938  fsetprcnexALT  44171  f1cof1b  44184  reuf1odnf  44214  2reuimp  44222  ralbinrald  44229  afvco2  44283  dfatdmfcoafv2  44361  recnmulnred  44413  sqrtnegnre  44415  subsubelfzo0  44434  ichcircshi  44522  sprvalpwle2  44557  sprsymrelf1lem  44559  sbcpr  44589  poprelb  44592  31prm  44665  requad01  44689  dfeven3  44726  iseven5  44732  0noddALTV  44757  2noddALTV  44761  fpprmod  44795  sbgoldbaltlem1  44847  bgoldbtbndlem2  44874  isomuspgrlem2d  44899  0nodd  44980  2nodd  44982  isassintop  45020  rnghmf1o  45077  isrngim  45078  uzlidlring  45103  funcringcsetcALTV2lem8  45217  funcringcsetclem8ALTV  45240  nn0sumltlt  45302  ply1mulgsumlem2  45344  islindeps  45410  lindslinindsimp1  45414  lindslinindsimp2  45420  snlindsntor  45428  zlmodzxznm  45454  ldepslinc  45466  difmodm1lt  45484  elbigo2  45514  elbigolo1  45519  logblt1b  45526  fldivexpfllog2  45527  nnolog2flm1  45552  digexp  45569  nn0sumshdiglemB  45582  itsclquadeu  45739  itscnhlinecirc02p  45747  ipolublem  45888  ipoglblem  45891