Theorem bicomd 225

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  impbid2  228  imbitrrid  248  ibir  270  bitr2d  282  bitr3d  283  bitr4d  284  bitr2id  286  bitr2di  290  con1bid  357  pm5.5  363  imnot  367  baibr  544  rbaib  546  baibd  547  anabs5  673  annotanannot  845  pm5.55  961  pm5.54  1031  ninba  1035  pm5.75  1042  sbequ12r  2287  sbal1  2559  euor2  2640  eqabcdv  2896  necon3bbid  2994  necon4bbid  2998  ralanid  3110  rexanid  3111  sbralieALT  3341  ralcom2  3364  rmoanid  3377  reuanid  3378  rabrabi  3433  gencbvex  3510  alexeqg  3610  clel2g  3618  clel3g  3620  clel4g  3622  reurab  3664  reu8  3696  sbceq2a  3756  sbcco2  3771  reu8nf  3830  notabw  4265  2reu4lem  4477  reurexprg  4663  raltpd  4740  ssdifsn  4748  uniprg  4881  disjxun  5098  opabidw  5494  opabid  5495  soeq2  5577  sotrine  5595  posn  5733  xpiindi  5807  dmopab2rex  5893  elpredg  6302  fvopab6  7010  cbvfo  7273  f1eqcocnv  7285  isoid  7313  isoini  7322  isosolem  7331  riotaeqimp  7379  riotarab  7395  resoprab2  7515  tfisi  7839  tfinds2  7844  f1oweALT  7953  dfoprab3  8035  opiota  8040  mpof1o2d  8105  xpord2indlem  8127  xpord3inddlem  8134  mpocurryd  8249  oalimcl  8529  omword  8539  oeword  8560  nnacan  8598  nnmcan  8604  mapsnd  8868  findcard2s  9134  funisfsupp  9313  suppeqfsuppbi  9325  eqinf  9431  inflb  9436  infglb  9437  infglbb  9438  infltoreq  9450  infempty  9455  brwdomn0  9517  cantnfp1lem3  9635  ssrankr1  9793  r1pw  9803  djulf1o  9870  djurf1o  9871  aleph11  10040  alephval3  10066  gch-kn  10635  wunex2  10696  lttri2  11265  wloglei  11719  divne0b  11856  lemul1  12043  nnnle0  12246  div4p1lem1div2  12476  nn0ind-raph  12673  zindd  12674  suprfinzcl  12687  rebtwnz  12948  qreccl  12970  elpq  12976  xrlttri2  13144  2resupmax  13191  xmulneg1  13272  iooshf  13430  difreicc  13488  fzofzim  13715  elfzomelpfzo  13778  elfznelfzo  13779  zmodid2  13909  2submod  13945  modfzo0difsn  13956  om2uzlti  13963  expcan  14182  hashvnfin  14373  hashneq0  14377  prhash2ex  14412  hashgt0elex  14414  hashgt12el  14435  hashgt12el2  14436  hashbclem  14465  hashf1lem2  14469  prprrab  14486  swrd0  14672  pfxn0  14700  swrdswrd  14718  pfxccat3  14747  repswswrd  14797  cshf1  14823  cshw1repsw  14836  relexpindlem  15076  sgnneg  15113  sgn3da  15114  absz  15338  iserex  15684  prodrb  15962  absdvdsb  16308  dvdsabsb  16309  modmulconst  16322  dvdsadd  16336  dvdsabseq  16347  mod2eq0even  16380  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  zeo5  16390  sadadd2lem2  16484  smupvallem  16517  gcdass  16581  lcmdvds  16642  lcmass  16648  divgcdcoprm0  16699  divgcdcoprmex  16700  1nprm  16713  dvdsnprmd  16724  prmdvdssq  16753  ncoprmlnprm  16763  isevengcd2  16765  m1dvdsndvds  16834  cshws0  17137  sbcie3s  17198  dfiso2  17805  initoid  18034  termoid  18035  funcestrcsetclem8  18179  lublecllem  18390  odudlatb  18557  sgrppropd  18765  issubm2  18838  mgm2nsgrplem2  18956  nsgacs  19203  cycsubg2  19251  gapm  19346  sscntz  19366  pgrpsubgsymgbi  19448  f1omvdcnv  19484  pmtrprfvalrn  19528  odval2  19591  lsmcntz  19719  rngpropd  20220  rnghmf1o  20501  isrngim2  20502  rhmf1o  20540  isrim  20541  dfprm2  21525  pzriprnglem10  21542  psgnfix2  21651  islinds3  21886  islindf4  21890  snifpsrbag  21972  gsumply1eq  22372  mdetdiaglem  22658  mdetunilem9  22680  slesolinv  22740  slesolex  22742  cpmatel2  22773  m2cpmghm  22804  m2cpminvid2  22815  pm2mpf1  22859  chfacfscmul0  22918  chfacfscmulfsupp  22919  chfacfpmmul0  22922  chfacfpmmulfsupp  22923  isopn2  23092  cmpsub  23460  connsub  23481  ncvs1  25219  rrxmvallem  25466  itg1mulc  25766  lhop1  26076  mdegleb  26124  lawcos  26881  leibpi  27007  2lgslem1a  27455  2sq2  27497  lestric  27832  bdayons  28369  n0subs2  28457  bdaypw2n0bndlem  28556  colinearalg  29111  edg0iedg0  29256  uhgreq12g  29266  uhgrvtxedgiedgb  29337  usgredg2v  29428  edg0usgr  29454  dfnbgr2  29538  nbuhgr  29544  nbusgredgeu0  29569  nb3grprlem1  29581  nb3grpr  29583  uvtx2vtx1edgb  29600  redwlk  29871  uhgrwkspthlem2  29954  usgr2wlkspth  29959  pthdlem1  29966  cyclnspth  30001  crctcshwlkn0lem1  30010  crctcshwlkn0lem4  30013  crctcsh  30024  iswwlksnx  30040  wwlksm1edg  30081  wwlksnextsurj  30100  wwlksnextproplem3  30111  2wlkdlem4  30128  2wlkdlem5  30129  2pthdlem1  30130  s3wwlks2on  30156  sps3wwlks2on  30157  wpthswwlks2on  30164  elwspths2spth  30170  rusgrnumwwlks  30177  umgrclwwlkge2  30193  clwlkclwwlklem2a4  30199  clwlkclwwlk  30204  clwlkclwwlkflem  30206  clwwisshclwws  30217  isclwwlknx  30238  clwwlknwwlksnb  30257  eclclwwlkn1  30277  clwwlknonel  30297  clwwlknun  30314  3wlkdlem6  30367  frgrncvvdeqlem9  30509  fusgreg2wsp  30538  numclwwlk2lem1lem  30544  extwwlkfab  30554  frgrreggt1  30595  ubthlem1  31073  norm-i  31332  hoeq  31963  nmopgt0  32115  pjimai  32379  chirredi  32597  addltmulALT  32649  opreu2reuALT  32676  sbcies  32687  rmounid  32694  iunrdx  32763  disjrdx  32791  archiabl  33378  islbs5  33566  ist0cld  34130  oms0  34594  eulerpartgbij  34669  reprinrn  34912  usgrgt2cycl  35480  satfv1lem  35712  satf0op  35727  dmopab3rexdif  35755  satefvfmla0  35768  mrsubrn  35863  topfne  36714  unbdqndv1  36946  bj-hbntbi  37179  bj-issetwt  37360  bj-clel3gALT  37533  copsex2d  37631  bj-elid6  37662  dfgcd3  37816  topdifinfeq  37844  wl-sbalnae  38065  sin2h  38109  poimirlem16  38135  poimirlem17  38136  poimirlem25  38144  mbfresfi  38165  itg2addnclem  38170  itg2addnclem2  38171  itg2addnclem3  38172  ftc1anclem1  38192  isidlc  38514  eldmressnALTV  38778  islshpsm  39604  lshpkrlem1  39734  opcon1b  39822  lautlt  40715  lauteq  40719  idlaut  40720  diblsmopel  41795  doch11  41997  recbothd  42609  aks4d1p8d2  42702  aks4d1p8  42704  isprimroot2  42711  posbezout  42717  aks6d1c5lem1  42753  sticksstones1  42763  sticksstones11  42773  sticksstones22  42785  aks6d1c6lem3  42789  aks6d1c6lem4  42790  aks6d1c7  42801  aks5lem8  42818  dvdsexpnn0  42943  redvmptabs  42969  redivne0bd  43059  prjsprellsp  43193  prjspeclsp  43194  abbibw  43259  istopclsd  43281  eqrabdioph  43358  rexzrexnn0  43381  zindbi  43523  expdiophlem2  43599  onsupeqmax  43823  onsupeqnmax  43824  ordeldif  43835  infordmin  44108  inintabd  44155  cnvcnvintabd  44176  cnvintabd  44179  sqrtcvallem1  44207  reabsifneg  44208  fsovrfovd  44585  ntrclsiso  44643  ntrneifv3  44658  ntrneineine0lem  44659  ntrneicls11  44666  suprleubrd  44742  suprlubrd  44744  lemuldiv4d  44747  pm14.122a  44998  3impexpbicomi  45057  onfrALTlem5  45118  bitr3VD  45424  onfrALTlem5VD  45460  csbrngVD  45471  pwpwuni  45637  supxrre3  45901  xrralrecnnge  45965  eliooshift  46082  limsupre2lem  46298  liminflimsupclim  46381  xlimbr  46401  smfrec  47363  fsetprcnexALT  47656  f1cof1b  47671  reuf1odnf  47701  2reuimp  47709  ralbinrald  47716  afvco2  47770  dfatdmfcoafv2  47848  recnmulnred  47899  sqrtnegnre  47901  subsubelfzo0  47921  ceilbi  47931  ichcircshi  48060  sprvalpwle2  48095  sprsymrelf1lem  48097  sbcpr  48127  poprelb  48130  31prm  48206  requad01  48243  dfeven3  48280  iseven5  48286  0noddALTV  48311  2noddALTV  48315  fpprmod  48349  sbgoldbaltlem1  48401  bgoldbtbndlem2  48428  dfclnbgr2  48445  dfsclnbgr2  48468  dfvopnbgr2  48475  dfsclnbgr6  48480  isuspgrim0lem  48515  usgrgrtrirex  48572  usgrexmpl2nb1  48654  usgrexmpl2nb2  48655  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  pgn4cyclex  48748  0nodd  48792  2nodd  48794  isassintop  48832  uzlidlring  48857  funcringcsetcALTV2lem8  48919  funcringcsetclem8ALTV  48942  nn0sumltlt  48972  ply1mulgsumlem2  49009  islindeps  49075  lindslinindsimp1  49079  lindslinindsimp2  49085  snlindsntor  49093  zlmodzxznm  49119  ldepslinc  49131  elbigo2  49174  elbigolo1  49179  logblt1b  49186  fldivexpfllog2  49187  nnolog2flm1  49212  digexp  49229  nn0sumshdiglemB  49242  itsclquadeu  49399  itscnhlinecirc02p  49407  ipolublem  49607  ipoglblem  49610