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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used 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  546  rbaib  548  baibd  549  anabs5  676  annotanannot  848  pm5.55  963  pm5.54  1035  ninba  1039  pm5.75  1046  sbequ12r  2290  sbal1  2562  euor2  2643  eqabcdv  2899  necon3bbid  2997  necon4bbid  3001  ralanid  3115  rexanid  3116  sbralieALT  3345  ralcom2  3368  rmoanid  3381  reuanid  3382  rabrabi  3437  gencbvex  3513  alexeqg  3612  clel2g  3620  clel3g  3622  clel4g  3624  reurab  3666  reu8  3698  sbceq2a  3758  sbcco2  3773  reu8nf  3831  notabw  4266  2reu4lem  4486  reurexprg  4672  raltpd  4749  ssdifsn  4758  uniprg  4890  disjxun  5109  opabidw  5510  opabid  5511  soeq2  5593  sotrine  5611  posn  5749  xpiindi  5823  dmopab2rex  5909  elpredg  6320  fvopab6  7028  cbvfo  7296  f1eqcocnv  7308  isoid  7336  isoini  7345  isosolem  7354  riotaeqimp  7402  riotarab  7418  resoprab2  7538  tfisi  7861  tfinds2  7866  f1oweALT  7975  dfoprab3  8057  opiota  8062  mpof1o2d  8127  xpord2indlem  8149  xpord3inddlem  8156  mpocurryd  8271  oalimcl  8551  omword  8561  oeword  8582  nnacan  8620  nnmcan  8626  mapsnd  8890  findcard2s  9157  funisfsupp  9334  suppeqfsuppbi  9346  eqinf  9452  inflb  9457  infglb  9458  infglbb  9459  infltoreq  9471  infempty  9476  brwdomn0  9538  cantnfp1lem3  9656  ssrankr1  9814  r1pw  9824  djulf1o  9914  djurf1o  9915  aleph11  10084  alephval3  10110  gch-kn  10679  wunex2  10740  lttri2  11309  wloglei  11763  divne0b  11900  lemul1  12084  nnnle0  12286  div4p1lem1div2  12516  nn0ind-raph  12714  zindd  12715  suprfinzcl  12728  rebtwnz  12989  qreccl  13011  elpq  13017  xrlttri2  13185  2resupmax  13232  xmulneg1  13313  iooshf  13471  difreicc  13529  fzofzim  13757  elfzomelpfzo  13820  elfznelfzo  13821  zmodid2  13952  2submod  13988  modfzo0difsn  13999  om2uzlti  14006  expcan  14225  hashvnfin  14416  hashneq0  14420  prhash2ex  14455  hashgt0elex  14457  hashgt12el  14479  hashgt12el2  14480  hashbclem  14509  hashf1lem2  14513  prprrab  14530  swrd0  14720  pfxn0  14748  swrdswrd  14766  pfxccat3  14795  repswswrd  14847  cshf1  14873  cshw1repsw  14886  relexpindlem  15126  sgnneg  15163  sgn3da  15164  absz  15388  iserex  15734  prodrb  16011  absdvdsb  16356  dvdsabsb  16357  modmulconst  16370  dvdsadd  16384  dvdsabseq  16395  mod2eq0even  16428  oddnn02np1  16430  oddge22np1  16431  evennn02n  16432  evennn2n  16433  zeo5  16438  sadadd2lem2  16532  smupvallem  16565  gcdass  16629  lcmdvds  16690  lcmass  16696  divgcdcoprm0  16747  divgcdcoprmex  16748  1nprm  16761  dvdsnprmd  16772  prmdvdssq  16801  ncoprmlnprm  16811  isevengcd2  16813  m1dvdsndvds  16882  cshws0  17185  sbcie3s  17246  dfiso2  17853  initoid  18082  termoid  18083  funcestrcsetclem8  18227  lublecllem  18438  odudlatb  18605  sgrppropd  18823  issubm2  18901  mgm2nsgrplem2  19020  nsgacs  19274  cycsubg2  19327  gapm  19422  sscntz  19442  pgrpsubgsymgbi  19524  f1omvdcnv  19560  pmtrprfvalrn  19604  odval2  19667  lsmcntz  19795  rngpropd  20298  rnghmf1o  20582  isrngim2  20583  rhmf1o  20627  isrim  20628  df2idl2crng  21473  dfprm2  21675  pzriprnglem10  21692  psgnfix2  21801  islinds3  22036  islindf4  22040  snifpsrbag  22122  gsumply1eq  22521  mdetdiaglem  22807  mdetunilem9  22829  slesolinv  22889  slesolex  22891  cpmatel2  22922  m2cpmghm  22953  m2cpminvid2  22964  pm2mpf1  23008  chfacfscmul0  23067  chfacfscmulfsupp  23068  chfacfpmmul0  23071  chfacfpmmulfsupp  23072  isopn2  23241  cmpsub  23609  connsub  23630  ncvs1  25369  rrxmvallem  25616  itg1mulc  25916  lhop1  26226  mdegleb  26274  lawcos  27034  leibpi  27160  2lgslem1a  27608  2sq2  27650  lestric  27985  bdayons  28522  n0subs2  28610  bdaypw2n0bndlem  28709  colinearalg  29317  edg0iedg0  29462  uhgreq12g  29472  uhgrvtxedgiedgb  29543  usgredg2v  29637  edg0usgr  29663  dfnbgr2  29747  nbuhgr  29753  nbusgredgeu0  29778  nb3grprlem1  29790  nb3grpr  29792  uvtx2vtx1edgb  29809  redwlk  30080  uhgrwkspthlem2  30169  usgr2wlkspth  30174  pthdlem1  30181  cyclnspth  30218  crctcshwlkn0lem1  30228  crctcshwlkn0lem4  30231  crctcsh  30242  iswwlksnx  30258  wwlksm1edg  30299  wwlksnextsurj  30318  wwlksnextproplem3  30329  2wlkdlem4  30346  2wlkdlem5  30347  2pthdlem1  30348  s3wwlks2on  30374  sps3wwlks2on  30375  wpthswwlks2on  30382  elwspths2spth  30388  rusgrnumwwlks  30395  umgrclwwlkge2  30411  clwlkclwwlklem2a4  30417  clwlkclwwlk  30422  clwlkclwwlkflem  30424  clwwisshclwws  30435  isclwwlknx  30456  clwwlknwwlksnb  30475  eclclwwlkn1  30495  clwwlknonel  30515  clwwlknun  30532  3wlkdlem6  30589  frgrncvvdeqlem9  30731  fusgreg2wsp  30760  numclwwlk2lem1lem  30766  extwwlkfab  30776  frgrreggt1  30817  ubthlem1  31295  norm-i  31554  hoeq  32185  nmopgt0  32337  pjimai  32601  chirredi  32819  addltmulALT  32871  opreu2reuALT  32896  sbcies  32907  rmounid  32914  iunrdx  32981  disjrdx  33009  archiabl  33584  islbs5  33759  ist0cld  34289  oms0  34754  eulerpartgbij  34829  reprinrn  35072  usgrgt2cycl  35669  satfv1lem  35893  satf0op  35908  dmopab3rexdif  35936  satefvfmla0  35949  mrsubrn  36044  topfne  36924  unbdqndv1  37156  bj-hbntbi  37388  bj-issetwt  37569  bj-clel3gALT  37743  copsex2d  37842  bj-elid6  37873  dfgcd3  38027  topdifinfeq  38055  wl-sbalnae  38276  sin2h  38320  poimirlem16  38346  poimirlem17  38347  poimirlem25  38355  mbfresfi  38376  itg2addnclem  38381  itg2addnclem2  38382  itg2addnclem3  38383  ftc1anclem1  38403  findcard4  38424  isidlc  38726  eldmressnALTV  38988  islshpsm  39814  lshpkrlem1  39944  opcon1b  40032  lautlt  40925  lauteq  40929  idlaut  40930  diblsmopel  42005  doch11  42207  recbothd  42819  aks4d1p8d2  42912  aks4d1p8  42914  isprimroot2  42921  posbezout  42927  aks6d1c5lem1  42963  sticksstones1  42973  sticksstones11  42983  sticksstones22  42995  aks6d1c6lem3  42999  aks6d1c6lem4  43000  aks6d1c7  43011  aks5lem8  43028  dvdsexpnn0  43155  redvmptabs  43181  redivne0bd  43271  prjsprellsp  43403  prjspeclsp  43404  abbibw  43469  istopclsd  43491  eqrabdioph  43568  rexzrexnn0  43591  zindbi  43733  expdiophlem2  43809  onsupeqmax  44033  onsupeqnmax  44034  ordeldif  44045  infordmin  44318  inintabd  44365  cnvcnvintabd  44386  cnvintabd  44389  sqrtcvallem1  44417  reabsifneg  44418  fsovrfovd  44795  ntrclsiso  44853  ntrneifv3  44868  ntrneineine0lem  44869  ntrneicls11  44876  suprleubrd  44952  suprlubrd  44954  lemuldiv4d  44957  pm14.122a  45192  3impexpbicomi  45250  onfrALTlem5  45311  bitr3VD  45617  onfrALTlem5VD  45653  csbrngVD  45664  pwpwuni  45837  supxrre3  46101  xrralrecnnge  46165  eliooshift  46282  limsupre2lem  46498  liminflimsupclim  46581  xlimbr  46601  smfrec  47563  fsetprcnexALT  47859  f1cof1b  47874  reuf1odnf  47904  2reuimp  47912  ralbinrald  47919  afvco2  47973  dfatdmfcoafv2  48051  recnmulnred  48102  sqrtnegnre  48104  subsubelfzo0  48124  ceilbi  48134  ichcircshi  48263  sprvalpwle2  48298  sprsymrelf1lem  48300  sbcpr  48330  poprelb  48333  31prm  48409  requad01  48446  dfeven3  48483  iseven5  48489  0noddALTV  48514  2noddALTV  48518  fpprmod  48552  sbgoldbaltlem1  48604  bgoldbtbndlem2  48631  dfclnbgr2  48648  dfsclnbgr2  48671  dfvopnbgr2  48678  dfsclnbgr6  48683  isuspgrim0lem  48718  usgrgrtrirex  48775  usgrexmpl2nb1  48857  usgrexmpl2nb2  48858  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  pgn4cyclex  48951  0nodd  48994  2nodd  48996  isassintop  49034  uzlidlring  49059  funcringcsetcALTV2lem8  49121  funcringcsetclem8ALTV  49144  prmringnzring  49161  dfidom2  49167  idomcanl  49171  nn0sumltlt  49189  ply1mulgsumlem2  49226  islindeps  49292  lindslinindsimp1  49296  lindslinindsimp2  49302  snlindsntor  49310  zlmodzxznm  49336  ldepslinc  49348  elbigo2  49391  elbigolo1  49396  logblt1b  49403  fldivexpfllog2  49404  nnolog2flm1  49429  digexp  49446  nn0sumshdiglemB  49459  itsclquadeu  49616  itscnhlinecirc02p  49624  ipolublem  49823  ipoglblem  49826  ralrals  50645  rexrals  50646  ralals  50651  rexals  50652