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  2253  sbal1  2526  euor2  2606  eqabcdv  2862  necon3bbid  2962  necon4bbid  2966  ralanid  3077  rexanid  3078  sbralieALT  3327  ralcom2  3351  rmoanid  3364  reuanid  3365  rabrabi  3425  gencbvex  3507  sbhypfOLD  3511  alexeqg  3617  clel2g  3625  clel3g  3627  clel4g  3629  reurab  3672  reu8  3704  sbceq2a  3765  sbcco2  3780  reu8nf  3840  notabw  4276  2reu4lem  4485  reurexprg  4668  raltpd  4745  ssdifsn  4752  uniprg  4887  disjxun  5105  opabidw  5484  opabid  5485  soeq2  5568  sotrine  5586  posn  5724  xpiindi  5799  dmopab2rex  5881  elpredg  6288  fvopab6  7002  cbvfo  7264  f1eqcocnv  7276  isoid  7304  isoini  7313  isosolem  7322  riotaeqimp  7370  riotarab  7386  resoprab2  7508  tfisi  7835  tfinds2  7840  f1oweALT  7951  dfoprab3  8033  opiota  8038  xpord2indlem  8126  xpord3inddlem  8133  mpocurryd  8248  oalimcl  8524  omword  8534  oeword  8554  nnacan  8592  nnmcan  8598  mapsnd  8859  findcard2s  9129  funisfsupp  9318  suppeqfsuppbi  9330  eqinf  9436  inflb  9441  infglb  9442  infglbb  9443  infltoreq  9455  infempty  9460  brwdomn0  9522  cantnfp1lem3  9633  ssrankr1  9788  r1pw  9798  djulf1o  9865  djurf1o  9866  aleph11  10037  alephval3  10063  gch-kn  10630  wunex2  10691  lttri2  11256  wloglei  11710  divne0b  11848  lemul1  12034  nnnle0  12219  div4p1lem1div2  12437  nn0ind-raph  12634  zindd  12635  suprfinzcl  12648  rebtwnz  12906  qreccl  12928  elpq  12934  xrlttri2  13102  2resupmax  13148  xmulneg1  13229  iooshf  13387  difreicc  13445  fzofzim  13670  elfzomelpfzo  13732  elfznelfzo  13733  zmodid2  13861  2submod  13897  modfzo0difsn  13908  om2uzlti  13915  expcan  14134  hashvnfin  14325  hashneq0  14329  prhash2ex  14364  hashgt0elex  14366  hashgt12el  14387  hashgt12el2  14388  hashbclem  14417  hashf1lem2  14421  prprrab  14438  swrd0  14623  pfxn0  14651  swrdswrd  14670  pfxccat3  14699  repswswrd  14749  cshf1  14775  cshw1repsw  14788  relexpindlem  15029  absz  15277  iserex  15623  prodrb  15898  absdvdsb  16244  dvdsabsb  16245  modmulconst  16258  dvdsadd  16272  dvdsabseq  16283  mod2eq0even  16316  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  zeo5  16326  sadadd2lem2  16420  smupvallem  16453  gcdass  16517  lcmdvds  16578  lcmass  16584  divgcdcoprm0  16635  divgcdcoprmex  16636  1nprm  16649  dvdsnprmd  16660  prmdvdssq  16688  ncoprmlnprm  16698  isevengcd2  16700  m1dvdsndvds  16769  cshws0  17072  sbcie3s  17132  dfiso2  17734  initoid  17963  termoid  17964  funcestrcsetclem8  18108  lublecllem  18319  odudlatb  18484  sgrppropd  18658  issubm2  18731  mgm2nsgrplem2  18846  nsgacs  19094  cycsubg2  19142  gapm  19238  sscntz  19258  pgrpsubgsymgbi  19338  f1omvdcnv  19374  pmtrprfvalrn  19418  odval2  19481  lsmcntz  19609  rngpropd  20083  rnghmf1o  20361  isrngim2  20362  rhmf1o  20400  isrim  20401  isrimOLD  20402  dfprm2  21383  pzriprnglem10  21400  psgnfix2  21508  islinds3  21743  islindf4  21747  snifpsrbag  21829  gsumply1eq  22196  mdetdiaglem  22485  mdetunilem9  22507  slesolinv  22567  slesolex  22569  cpmatel2  22600  m2cpmghm  22631  m2cpminvid2  22642  pm2mpf1  22686  chfacfscmul0  22745  chfacfscmulfsupp  22746  chfacfpmmul0  22749  chfacfpmmulfsupp  22750  isopn2  22919  cmpsub  23287  connsub  23308  ncvs1  25057  rrxmvallem  25304  itg1mulc  25605  lhop1  25919  mdegleb  25969  lawcos  26726  leibpi  26852  2lgslem1a  27302  2sq2  27344  sletric  27676  bdayon  28173  n0subs2  28254  0reno  28348  colinearalg  28837  edg0iedg0  28982  uhgreq12g  28992  uhgrvtxedgiedgb  29063  usgredg2v  29154  edg0usgr  29180  dfnbgr2  29264  nbuhgr  29270  nbusgredgeu0  29295  nb3grprlem1  29307  nb3grpr  29309  uvtx2vtx1edgb  29326  redwlk  29600  uhgrwkspthlem2  29684  usgr2wlkspth  29689  pthdlem1  29696  cyclnspth  29731  crctcshwlkn0lem1  29740  crctcshwlkn0lem4  29743  crctcsh  29754  iswwlksnx  29770  wwlksm1edg  29811  wwlksnextsurj  29830  wwlksnextproplem3  29841  2wlkdlem4  29858  2wlkdlem5  29859  2pthdlem1  29860  s3wwlks2on  29886  wpthswwlks2on  29891  elwspths2spth  29897  rusgrnumwwlks  29904  umgrclwwlkge2  29920  clwlkclwwlklem2a4  29926  clwlkclwwlk  29931  clwlkclwwlkflem  29933  clwwisshclwws  29944  isclwwlknx  29965  clwwlknwwlksnb  29984  eclclwwlkn1  30004  clwwlknonel  30024  clwwlknun  30041  3wlkdlem6  30094  frgrncvvdeqlem9  30236  fusgreg2wsp  30265  numclwwlk2lem1lem  30271  extwwlkfab  30281  frgrreggt1  30322  ubthlem1  30799  norm-i  31058  hoeq  31689  nmopgt0  31841  pjimai  32105  chirredi  32323  addltmulALT  32375  bian1d  32385  opreu2reuALT  32406  sbcies  32417  rmounid  32424  iunrdx  32492  disjrdx  32520  sgnneg  32758  sgn3da  32759  archiabl  33152  islbs5  33351  ist0cld  33823  oms0  34288  eulerpartgbij  34363  reprinrn  34609  usgrgt2cycl  35117  satfv1lem  35349  satf0op  35364  dmopab3rexdif  35392  satefvfmla0  35405  mrsubrn  35500  topfne  36342  unbdqndv1  36496  bj-hbntbi  36692  bj-issetwt  36863  bj-clel3gALT  37036  copsex2d  37127  bj-elid6  37158  dfgcd3  37312  topdifinfeq  37338  wl-sbalnae  37550  sin2h  37604  poimirlem16  37630  poimirlem17  37631  poimirlem25  37639  mbfresfi  37660  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  ftc1anclem1  37687  isidlc  38009  eldmressnALTV  38261  islshpsm  38973  lshpkrlem1  39103  opcon1b  39191  lautlt  40085  lauteq  40089  idlaut  40090  diblsmopel  41165  doch11  41367  recbothd  41980  aks4d1p8d2  42073  aks4d1p8  42075  isprimroot2  42082  posbezout  42088  aks6d1c5lem1  42124  sticksstones1  42134  sticksstones11  42144  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c7  42172  aks5lem8  42189  f1o2d2  42221  dvdsexpnn0  42322  redvmptabs  42348  prjsprellsp  42599  prjspeclsp  42600  abbibw  42665  istopclsd  42688  eqrabdioph  42765  rexzrexnn0  42792  zindbi  42935  expdiophlem2  43011  onsupeqmax  43235  onsupeqnmax  43236  ordeldif  43247  infordmin  43521  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  sqrtcvallem1  43620  reabsifneg  43621  fsovrfovd  43998  ntrclsiso  44056  ntrneifv3  44071  ntrneineine0lem  44072  ntrneicls11  44079  suprleubrd  44155  suprlubrd  44157  lemuldiv4d  44160  pm14.122a  44411  3impexpbicomi  44471  onfrALTlem5  44532  bitr3VD  44838  onfrALTlem5VD  44874  csbrngVD  44885  pwpwuni  45051  supxrre3  45321  xrralrecnnge  45386  eliooshift  45504  limsupre2lem  45722  liminflimsupclim  45805  xlimbr  45825  smfrec  46787  fsetprcnexALT  47063  f1cof1b  47078  reuf1odnf  47108  2reuimp  47116  ralbinrald  47123  afvco2  47177  dfatdmfcoafv2  47255  recnmulnred  47306  sqrtnegnre  47308  subsubelfzo0  47327  ceilbi  47334  ichcircshi  47455  sprvalpwle2  47490  sprsymrelf1lem  47492  sbcpr  47522  poprelb  47525  31prm  47598  requad01  47622  dfeven3  47659  iseven5  47665  0noddALTV  47690  2noddALTV  47694  fpprmod  47728  sbgoldbaltlem1  47780  bgoldbtbndlem2  47807  dfclnbgr2  47824  dfsclnbgr2  47846  dfvopnbgr2  47853  dfsclnbgr6  47858  isuspgrim0lem  47893  usgrgrtrirex  47949  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgn4cyclex  48116  0nodd  48158  2nodd  48160  isassintop  48198  uzlidlring  48223  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  nn0sumltlt  48338  ply1mulgsumlem2  48376  islindeps  48442  lindslinindsimp1  48446  lindslinindsimp2  48452  snlindsntor  48460  zlmodzxznm  48486  ldepslinc  48498  elbigo2  48541  elbigolo1  48546  logblt1b  48553  fldivexpfllog2  48554  nnolog2flm1  48579  digexp  48596  nn0sumshdiglemB  48609  itsclquadeu  48766  itscnhlinecirc02p  48774  ipolublem  48974  ipoglblem  48977