Theorem bicomd 222

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 221	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  impbid2  225  imbitrrid  245  ibir  268  bitr2d  280  bitr3d  281  bitr4d  282  bitr2id  284  bitr2di  288  con1bid  356  pm5.5  362  imnot  366  baibr  538  rbaib  540  baibd  541  anabs5  662  annotanannot  834  pm5.55  948  pm5.54  1017  ninba  1021  pm5.75  1028  sbequ12r  2245  sbal1  2528  euor2  2610  eqabcdv  2869  necon3bbid  2979  necon4bbid  2983  ralanid  3096  rexanid  3097  sbralieALT  3356  ralcom2  3374  rmoanid  3387  reuanid  3388  rabrabi  3451  gencbvex  3536  sbhypfOLD  3540  alexeqg  3639  clel2g  3647  clel2gOLD  3648  clel3g  3650  clel4g  3652  reurab  3697  reu8  3729  sbceq2a  3789  sbcco2  3804  reu8nf  3871  notabw  4303  2reu4lem  4525  reurexprg  4708  raltpd  4785  ssdifsn  4791  uniprg  4925  disjxun  5146  opabidw  5524  opabid  5525  soeq2  5610  sotrine  5626  posn  5760  xpiindi  5834  dmopab2rex  5916  elpredg  6312  fvopab6  7029  cbvfo  7284  f1eqcocnv  7296  f1eqcocnvOLD  7297  isoid  7323  isoini  7332  isosolem  7341  riotaeqimp  7389  riotarab  7405  resoprab2  7524  tfisi  7845  tfinds2  7850  f1oweALT  7956  dfoprab3  8037  opiota  8042  xpord2indlem  8130  xpord3inddlem  8137  mpocurryd  8251  oalimcl  8557  omword  8567  oeword  8587  nnacan  8625  nnmcan  8631  mapsnd  8877  findcard2s  9162  funisfsupp  9364  suppeqfsuppbi  9374  eqinf  9476  inflb  9481  infglb  9482  infglbb  9483  infltoreq  9494  infempty  9499  brwdomn0  9561  cantnfp1lem3  9672  ssrankr1  9827  r1pw  9837  djulf1o  9904  djurf1o  9905  aleph11  10076  alephval3  10102  gch-kn  10669  wunex2  10730  lttri2  11293  wloglei  11743  divne0b  11880  lemul1  12063  nnnle0  12242  div4p1lem1div2  12464  nn0ind-raph  12659  zindd  12660  suprfinzcl  12673  rebtwnz  12928  qreccl  12950  elpq  12956  xrlttri2  13118  2resupmax  13164  xmulneg1  13245  iooshf  13400  difreicc  13458  fzofzim  13676  elfzomelpfzo  13733  elfznelfzo  13734  zmodid2  13861  2submod  13894  modfzo0difsn  13905  om2uzlti  13912  expcan  14131  hashvnfin  14317  hashneq0  14321  prhash2ex  14356  hashgt0elex  14358  hashgt12el  14379  hashgt12el2  14380  hashbclem  14408  hashf1lem2  14414  prprrab  14431  swrd0  14605  pfxn0  14633  swrdswrd  14652  pfxccat3  14681  repswswrd  14731  cshf1  14757  cshw1repsw  14770  relexpindlem  15007  absz  15255  iserex  15600  prodrb  15873  absdvdsb  16215  dvdsabsb  16216  modmulconst  16228  dvdsadd  16242  dvdsabseq  16253  mod2eq0even  16286  oddnn02np1  16288  oddge22np1  16289  evennn02n  16290  evennn2n  16291  zeo5  16296  sadadd2lem2  16388  smupvallem  16421  gcdass  16486  lcmdvds  16542  lcmass  16548  divgcdcoprm0  16599  divgcdcoprmex  16600  1nprm  16613  dvdsnprmd  16624  prmdvdssq  16652  ncoprmlnprm  16661  isevengcd2  16663  m1dvdsndvds  16728  cshws0  17032  sbcie3s  17092  dfiso2  17716  initoid  17948  termoid  17949  funcestrcsetclem8  18096  lublecllem  18310  odudlatb  18475  sgrppropd  18619  issubm2  18682  mgm2nsgrplem2  18797  nsgacs  19037  cycsubg2  19082  gapm  19165  sscntz  19185  pgrpsubgsymgbi  19271  f1omvdcnv  19307  pmtrprfvalrn  19351  odval2  19414  lsmcntz  19542  rhmf1o  20262  isrim  20263  isrimOLD  20264  dfprm2  21035  psgnfix2  21144  islinds3  21381  islindf4  21385  snifpsrbag  21467  gsumply1eq  21821  mdetdiaglem  22092  mdetunilem9  22114  slesolinv  22174  slesolex  22176  cpmatel2  22207  m2cpmghm  22238  m2cpminvid2  22249  pm2mpf1  22293  chfacfscmul0  22352  chfacfscmulfsupp  22353  chfacfpmmul0  22356  chfacfpmmulfsupp  22357  isopn2  22528  cmpsub  22896  connsub  22917  ncvs1  24666  rrxmvallem  24913  itg1mulc  25214  lhop1  25523  mdegleb  25574  lawcos  26311  leibpi  26437  2lgslem1a  26884  2sq2  26926  sletric  27257  colinearalg  28158  edg0iedg0  28305  uhgreq12g  28315  uhgrvtxedgiedgb  28386  usgredg2v  28474  edg0usgr  28500  dfnbgr2  28584  nbuhgr  28590  nbusgredgeu0  28615  nb3grprlem1  28627  nb3grpr  28629  uvtx2vtx1edgb  28646  redwlk  28919  uhgrwkspthlem2  29001  usgr2wlkspth  29006  pthdlem1  29013  cyclnspth  29047  crctcshwlkn0lem1  29054  crctcshwlkn0lem4  29057  crctcsh  29068  iswwlksnx  29084  wwlksm1edg  29125  wwlksnextsurj  29144  wwlksnextproplem3  29155  2wlkdlem4  29172  2wlkdlem5  29173  2pthdlem1  29174  s3wwlks2on  29200  wpthswwlks2on  29205  elwspths2spth  29211  rusgrnumwwlks  29218  umgrclwwlkge2  29234  clwlkclwwlklem2a4  29240  clwlkclwwlk  29245  clwlkclwwlkflem  29247  clwwisshclwws  29258  isclwwlknx  29279  clwwlknwwlksnb  29298  eclclwwlkn1  29318  clwwlknonel  29338  clwwlknun  29355  3wlkdlem6  29408  frgrncvvdeqlem9  29550  fusgreg2wsp  29579  numclwwlk2lem1lem  29585  extwwlkfab  29595  frgrreggt1  29636  ubthlem1  30111  norm-i  30370  hoeq  31001  nmopgt0  31153  pjimai  31417  chirredi  31635  addltmulALT  31687  opreu2reuALT  31705  sbcies  31716  rmounid  31723  iunrdx  31783  disjrdx  31810  cnvoprabOLD  31933  archiabl  32332  islbs5  32485  ist0cld  32802  oms0  33285  eulerpartgbij  33360  sgnneg  33528  sgn3da  33529  reprinrn  33619  usgrgt2cycl  34110  satfv1lem  34342  satf0op  34357  dmopab3rexdif  34385  satefvfmla0  34398  mrsubrn  34493  topfne  35228  unbdqndv1  35373  bj-hbntbi  35571  bj-issetwt  35743  bj-clel3gALT  35918  copsex2d  36009  bj-elid6  36040  dfgcd3  36194  topdifinfeq  36220  wl-sb6rft  36402  wl-sbalnae  36416  sin2h  36467  poimirlem16  36493  poimirlem17  36494  poimirlem25  36502  mbfresfi  36523  itg2addnclem  36528  itg2addnclem2  36529  itg2addnclem3  36530  ftc1anclem1  36550  isidlc  36872  eldmressnALTV  37129  islshpsm  37839  lshpkrlem1  37969  opcon1b  38057  lautlt  38951  lauteq  38955  idlaut  38956  diblsmopel  40031  doch11  40233  recbothd  40847  aks4d1p8d2  40939  aks4d1p8  40941  sticksstones1  40951  sticksstones11  40961  sticksstones22  40973  metakunt16  40989  f1o2d2  41053  dvdsexpnn0  41228  prjsprellsp  41350  prjspeclsp  41351  istopclsd  41424  eqrabdioph  41501  rexzrexnn0  41528  zindbi  41671  expdiophlem2  41747  onsupeqmax  41981  onsupeqnmax  41982  ordeldif  41994  infordmin  42269  inintabd  42316  cnvcnvintabd  42337  cnvintabd  42340  sqrtcvallem1  42368  reabsifneg  42369  fsovrfovd  42746  ntrclsiso  42804  ntrneifv3  42819  ntrneineine0lem  42820  ntrneicls11  42827  suprleubrd  42904  suprlubrd  42906  lemuldiv4d  42909  pm14.122a  43167  3impexpbicomi  43227  onfrALTlem5  43289  bitr3VD  43596  onfrALTlem5VD  43632  csbrngVD  43643  pwpwuni  43730  supxrre3  44022  xrralrecnnge  44087  eliooshift  44206  limsupre2lem  44427  liminflimsupclim  44510  xlimbr  44530  smfrec  45492  fsetprcnexALT  45759  f1cof1b  45772  reuf1odnf  45802  2reuimp  45810  ralbinrald  45817  afvco2  45871  dfatdmfcoafv2  45949  recnmulnred  46000  sqrtnegnre  46002  subsubelfzo0  46021  ichcircshi  46109  sprvalpwle2  46144  sprsymrelf1lem  46146  sbcpr  46176  poprelb  46179  31prm  46252  requad01  46276  dfeven3  46313  iseven5  46319  0noddALTV  46344  2noddALTV  46348  fpprmod  46382  sbgoldbaltlem1  46434  bgoldbtbndlem2  46461  isomuspgrlem2d  46486  0nodd  46567  2nodd  46569  isassintop  46607  rngpropd  46660  rnghmf1o  46687  isrngim  46688  uzlidlring  46781  funcringcsetcALTV2lem8  46895  funcringcsetclem8ALTV  46918  nn0sumltlt  46980  ply1mulgsumlem2  47022  islindeps  47088  lindslinindsimp1  47092  lindslinindsimp2  47098  snlindsntor  47106  zlmodzxznm  47132  ldepslinc  47144  difmodm1lt  47162  elbigo2  47192  elbigolo1  47197  logblt1b  47204  fldivexpfllog2  47205  nnolog2flm1  47230  digexp  47247  nn0sumshdiglemB  47260  itsclquadeu  47417  itscnhlinecirc02p  47425  ipolublem  47565  ipoglblem  47568