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  imbitrrid  249  ibir  271  bitr2d  283  bitr3d  284  bitr4d  285  bitr2id  287  bitr2di  291  con1bid  358  pm5.5  364  imnot  368  baibr  545  rbaib  547  baibd  548  anabs5  675  annotanannot  847  pm5.55  963  pm5.54  1035  ninba  1039  pm5.75  1046  sbequ12r  2288  sbal1  2560  euor2  2641  eqabcdv  2897  necon3bbid  2995  necon4bbid  2999  ralanid  3113  rexanid  3114  sbralieALT  3343  ralcom2  3366  rmoanid  3379  reuanid  3380  rabrabi  3435  gencbvex  3511  alexeqg  3610  clel2g  3618  clel3g  3620  clel4g  3622  reurab  3664  reu8  3696  sbceq2a  3756  sbcco2  3771  reu8nf  3830  notabw  4266  2reu4lem  4484  reurexprg  4670  raltpd  4747  ssdifsn  4756  uniprg  4888  disjxun  5107  opabidw  5508  opabid  5509  soeq2  5591  sotrine  5609  posn  5747  xpiindi  5821  dmopab2rex  5907  elpredg  6316  fvopab6  7024  cbvfo  7287  f1eqcocnv  7299  isoid  7327  isoini  7336  isosolem  7345  riotaeqimp  7393  riotarab  7409  resoprab2  7529  tfisi  7851  tfinds2  7856  f1oweALT  7965  dfoprab3  8047  opiota  8052  mpof1o2d  8117  xpord2indlem  8139  xpord3inddlem  8146  mpocurryd  8261  oalimcl  8541  omword  8551  oeword  8572  nnacan  8610  nnmcan  8616  mapsnd  8880  findcard2s  9146  funisfsupp  9323  suppeqfsuppbi  9335  eqinf  9441  inflb  9446  infglb  9447  infglbb  9448  infltoreq  9460  infempty  9465  brwdomn0  9527  cantnfp1lem3  9645  ssrankr1  9803  r1pw  9813  djulf1o  9894  djurf1o  9895  aleph11  10064  alephval3  10090  gch-kn  10657  wunex2  10718  lttri2  11287  wloglei  11741  divne0b  11878  lemul1  12062  nnnle0  12264  div4p1lem1div2  12494  nn0ind-raph  12691  zindd  12692  suprfinzcl  12705  rebtwnz  12966  qreccl  12988  elpq  12994  xrlttri2  13162  2resupmax  13209  xmulneg1  13290  iooshf  13448  difreicc  13506  fzofzim  13734  elfzomelpfzo  13797  elfznelfzo  13798  zmodid2  13928  2submod  13964  modfzo0difsn  13975  om2uzlti  13982  expcan  14201  hashvnfin  14392  hashneq0  14396  prhash2ex  14431  hashgt0elex  14433  hashgt12el  14455  hashgt12el2  14456  hashbclem  14485  hashf1lem2  14489  prprrab  14506  swrd0  14692  pfxn0  14720  swrdswrd  14738  pfxccat3  14767  repswswrd  14817  cshf1  14843  cshw1repsw  14856  relexpindlem  15096  sgnneg  15133  sgn3da  15134  absz  15358  iserex  15704  prodrb  15982  absdvdsb  16327  dvdsabsb  16328  modmulconst  16341  dvdsadd  16355  dvdsabseq  16366  mod2eq0even  16399  oddnn02np1  16401  oddge22np1  16402  evennn02n  16403  evennn2n  16404  zeo5  16409  sadadd2lem2  16503  smupvallem  16536  gcdass  16600  lcmdvds  16661  lcmass  16667  divgcdcoprm0  16718  divgcdcoprmex  16719  1nprm  16732  dvdsnprmd  16743  prmdvdssq  16772  ncoprmlnprm  16782  isevengcd2  16784  m1dvdsndvds  16853  cshws0  17156  sbcie3s  17217  dfiso2  17824  initoid  18053  termoid  18054  funcestrcsetclem8  18198  lublecllem  18409  odudlatb  18576  sgrppropd  18784  issubm2  18857  mgm2nsgrplem2  18976  nsgacs  19223  cycsubg2  19276  gapm  19371  sscntz  19391  pgrpsubgsymgbi  19473  f1omvdcnv  19509  pmtrprfvalrn  19553  odval2  19616  lsmcntz  19744  rngpropd  20247  rnghmf1o  20530  isrngim2  20531  rhmf1o  20575  isrim  20576  df2idl2crng  21421  dfprm2  21623  pzriprnglem10  21640  psgnfix2  21749  islinds3  21984  islindf4  21988  snifpsrbag  22070  gsumply1eq  22469  mdetdiaglem  22755  mdetunilem9  22777  slesolinv  22837  slesolex  22839  cpmatel2  22870  m2cpmghm  22901  m2cpminvid2  22912  pm2mpf1  22956  chfacfscmul0  23015  chfacfscmulfsupp  23016  chfacfpmmul0  23019  chfacfpmmulfsupp  23020  isopn2  23189  cmpsub  23557  connsub  23578  ncvs1  25316  rrxmvallem  25563  itg1mulc  25863  lhop1  26173  mdegleb  26221  lawcos  26981  leibpi  27107  2lgslem1a  27555  2sq2  27597  lestric  27932  bdayons  28469  n0subs2  28557  bdaypw2n0bndlem  28656  colinearalg  29260  edg0iedg0  29405  uhgreq12g  29415  uhgrvtxedgiedgb  29486  usgredg2v  29577  edg0usgr  29603  dfnbgr2  29687  nbuhgr  29693  nbusgredgeu0  29718  nb3grprlem1  29730  nb3grpr  29732  uvtx2vtx1edgb  29749  redwlk  30020  uhgrwkspthlem2  30103  usgr2wlkspth  30108  pthdlem1  30115  cyclnspth  30150  crctcshwlkn0lem1  30159  crctcshwlkn0lem4  30162  crctcsh  30173  iswwlksnx  30189  wwlksm1edg  30230  wwlksnextsurj  30249  wwlksnextproplem3  30260  2wlkdlem4  30277  2wlkdlem5  30278  2pthdlem1  30279  s3wwlks2on  30305  sps3wwlks2on  30306  wpthswwlks2on  30313  elwspths2spth  30319  rusgrnumwwlks  30326  umgrclwwlkge2  30342  clwlkclwwlklem2a4  30348  clwlkclwwlk  30353  clwlkclwwlkflem  30355  clwwisshclwws  30366  isclwwlknx  30387  clwwlknwwlksnb  30406  eclclwwlkn1  30426  clwwlknonel  30446  clwwlknun  30463  3wlkdlem6  30516  frgrncvvdeqlem9  30658  fusgreg2wsp  30687  numclwwlk2lem1lem  30693  extwwlkfab  30703  frgrreggt1  30744  ubthlem1  31222  norm-i  31481  hoeq  32112  nmopgt0  32264  pjimai  32528  chirredi  32746  addltmulALT  32798  opreu2reuALT  32823  sbcies  32834  rmounid  32841  iunrdx  32908  disjrdx  32936  archiabl  33518  islbs5  33693  ist0cld  34223  oms0  34687  eulerpartgbij  34762  reprinrn  35005  usgrgt2cycl  35622  satfv1lem  35854  satf0op  35869  dmopab3rexdif  35897  satefvfmla0  35910  mrsubrn  36005  topfne  36885  unbdqndv1  37117  bj-hbntbi  37349  bj-issetwt  37530  bj-clel3gALT  37704  copsex2d  37803  bj-elid6  37834  dfgcd3  37988  topdifinfeq  38016  wl-sbalnae  38237  sin2h  38281  poimirlem16  38307  poimirlem17  38308  poimirlem25  38316  mbfresfi  38337  itg2addnclem  38342  itg2addnclem2  38343  itg2addnclem3  38344  ftc1anclem1  38364  isidlc  38686  eldmressnALTV  38948  islshpsm  39774  lshpkrlem1  39904  opcon1b  39992  lautlt  40885  lauteq  40889  idlaut  40890  diblsmopel  41965  doch11  42167  recbothd  42779  aks4d1p8d2  42872  aks4d1p8  42874  isprimroot2  42881  posbezout  42887  aks6d1c5lem1  42923  sticksstones1  42933  sticksstones11  42943  sticksstones22  42955  aks6d1c6lem3  42959  aks6d1c6lem4  42960  aks6d1c7  42971  aks5lem8  42988  dvdsexpnn0  43115  redvmptabs  43141  redivne0bd  43231  prjsprellsp  43363  prjspeclsp  43364  abbibw  43429  istopclsd  43451  eqrabdioph  43528  rexzrexnn0  43551  zindbi  43693  expdiophlem2  43769  onsupeqmax  43993  onsupeqnmax  43994  ordeldif  44005  infordmin  44278  inintabd  44325  cnvcnvintabd  44346  cnvintabd  44349  sqrtcvallem1  44377  reabsifneg  44378  fsovrfovd  44755  ntrclsiso  44813  ntrneifv3  44828  ntrneineine0lem  44829  ntrneicls11  44836  suprleubrd  44912  suprlubrd  44914  lemuldiv4d  44917  pm14.122a  45152  3impexpbicomi  45210  onfrALTlem5  45271  bitr3VD  45577  onfrALTlem5VD  45613  csbrngVD  45624  pwpwuni  45797  supxrre3  46061  xrralrecnnge  46125  eliooshift  46242  limsupre2lem  46458  liminflimsupclim  46541  xlimbr  46561  smfrec  47523  fsetprcnexALT  47819  f1cof1b  47834  reuf1odnf  47864  2reuimp  47872  ralbinrald  47879  afvco2  47933  dfatdmfcoafv2  48011  recnmulnred  48062  sqrtnegnre  48064  subsubelfzo0  48084  ceilbi  48094  ichcircshi  48223  sprvalpwle2  48258  sprsymrelf1lem  48260  sbcpr  48290  poprelb  48293  31prm  48369  requad01  48406  dfeven3  48443  iseven5  48449  0noddALTV  48474  2noddALTV  48478  fpprmod  48512  sbgoldbaltlem1  48564  bgoldbtbndlem2  48591  dfclnbgr2  48608  dfsclnbgr2  48631  dfvopnbgr2  48638  dfsclnbgr6  48643  isuspgrim0lem  48678  usgrgrtrirex  48735  usgrexmpl2nb1  48817  usgrexmpl2nb2  48818  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgnbgreunbgrlem2lem3  48901  pgn4cyclex  48911  0nodd  48955  2nodd  48957  isassintop  48995  uzlidlring  49020  funcringcsetcALTV2lem8  49082  funcringcsetclem8ALTV  49105  prmringnzring  49122  dfidom2  49128  idomcanl  49132  nn0sumltlt  49150  ply1mulgsumlem2  49187  islindeps  49253  lindslinindsimp1  49257  lindslinindsimp2  49263  snlindsntor  49271  zlmodzxznm  49297  ldepslinc  49309  elbigo2  49352  elbigolo1  49357  logblt1b  49364  fldivexpfllog2  49365  nnolog2flm1  49390  digexp  49407  nn0sumshdiglemB  49420  itsclquadeu  49577  itscnhlinecirc02p  49585  ipolublem  49784  ipoglblem  49787  ralrals  50606  rexrals  50607  ralals  50612  rexals  50613