MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomd Structured version   Visualization version   GIF version

Theorem bicomd 212
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
StepHypRef Expression
1 bicomd.1 . 2 (𝜑 → (𝜓𝜒))
2 bicom 211 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 207 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  impbid2  215  syl5ibr  235  ibir  256  bitr2d  268  bitr3d  269  bitr4d  270  syl5rbb  272  syl6rbb  276  con1bid  344  pm5.5  350  imnot  354  anabs5  847  pm5.55  937  pm5.54  941  baibr  943  rbaib  945  baibd  946  rbaibd  947  pm5.75  974  pm5.75OLD  975  ninba  996  sbequ12r  2098  cbvalv  2261  sbal1  2448  euor2  2502  abbi1dv  2730  necon3bbid  2819  necon4bbid  2823  ralcom2  3083  gencbvex  3223  sbhypf  3226  alexeqg  3302  clel3g  3310  reu8  3369  sbceq2a  3414  sbcco2  3426  raltpd  4258  disjxun  4581  opabid  4907  soeq2  4979  posn  5110  xpiindi  5179  fvopab6  6218  cbvfo  6444  f1eqcocnv  6456  isoid  6479  isoini  6488  isosolem  6497  resoprab2  6655  tfisi  6950  tfinds2  6955  f1oweALT  7043  dfoprab3  7115  opiota  7118  mpt2curryd  7282  oalimcl  7527  omword  7537  oeword  7557  nnacan  7595  nnmcan  7601  findcard2s  8086  funisfsupp  8163  suppeqfsuppbi  8172  eqinf  8273  inflb  8278  infglb  8279  infglbb  8280  infltoreq  8291  infempty  8295  brwdomn0  8357  cantnfp1lem3  8460  ssrankr1  8581  r1pw  8591  aleph11  8790  alephval3  8816  gch-kn  9378  wunex2  9439  lttri2  9999  wloglei  10439  divne0b  10575  lemul1  10754  nnnle0  10928  div4p1lem1div2  11164  nn0ind-raph  11353  zindd  11354  suprfinzcl  11368  rebtwnz  11663  qreccl  11684  xrlttri2  11851  2resupmax  11893  xmulneg1  11971  iooshf  12123  difreicc  12175  fzofzim  12382  elfzomelpfzo  12438  elfznelfzo  12439  divfl0  12487  zmodid2  12560  2submod  12593  modfzo0difsn  12604  om2uzlti  12611  expcan  12775  hashvnfin  13012  hashneq0  13016  prhash2ex  13048  hashgt0elex  13050  hashgt12el  13070  hashgt12el2  13071  hashbclem  13093  hashf1lem2  13097  prprrab  13112  swrdn0  13282  swrd0  13286  2swrdeqwrdeq  13305  swrdswrd  13312  swrdccat3  13343  repswswrd  13382  cshf1  13407  cshw1repsw  13420  relexpindlem  13651  absz  13899  iserex  14235  prodrb  14501  absdvdsb  14838  dvdsabsb  14839  modmulconst  14851  dvdsadd  14862  dvdsabseq  14873  mod2eq0even  14908  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  zeo5  14918  sadadd2lem2  15010  smupvallem  15043  gcdass  15102  lcmdvds  15159  lcmass  15165  divgcdcoprm0  15217  divgcdcoprmex  15218  1nprm  15230  dvdsnprmd  15241  ncoprmlnprm  15274  isevengcd2  15276  m1dvdsndvds  15341  cshws0  15646  sbcie2s  15744  sbcie3s  15745  dfiso2  16255  initoid  16478  termoid  16479  funcestrcsetclem8  16610  lublecllem  16811  odudlatb  17019  issubm2  17171  mgm2nsgrplem2  17229  nsgacs  17453  cycsubg2  17454  gapm  17562  sscntz  17582  pgrpsubgsymgbi  17650  f1omvdcnv  17687  pmtrprfvalrn  17731  odval2  17793  lsmcntz  17915  rhmf1o  18555  isrim  18556  snifpsrbag  19187  gsumply1eq  19496  dfprm2  19661  psgnfix2  19764  islinds3  19992  islindf4  19996  mdetdiaglem  20223  mdetunilem9  20245  slesolinv  20305  slesolex  20307  cpmatel2  20337  m2cpmghm  20368  m2cpminvid2  20379  pm2mpf1  20423  chfacfscmul0  20482  chfacfscmulfsupp  20483  chfacfpmmul0  20486  chfacfpmmulfsupp  20487  isopn2  20646  cmpsub  21013  connsub  21034  ncvs1  22765  rrxmvallem  22995  itg1mulc  23277  lhop1  23581  mdegleb  23628  lawcos  24346  leibpi  24469  2lgslem1a  24916  iscgra  25501  colinearalg  25590  uhgreq12g  25731  edg0iedg0  25800  uhgrvtxedgiedgb  25810  ausisusgra  25884  usgraedg4  25916  usgraidx2v  25922  nbgraf1olem1  25970  nb3graprlem1  25980  nb3grapr  25982  nb3grapr2  25983  cusgrarn  25988  uvtx01vtx  26020  redwlk  26136  wlkdvspthlem  26137  wlkdvspth  26138  wlkiswwlk1  26218  2wlkeq  26235  wwlkextsur  26259  wwlkm1edg  26263  wwlkextproplem3  26271  clwlkisclwwlklem2a4  26312  clwlkisclwwlk  26317  eclclwwlkn1  26359  clwlkfoclwwlk  26372  el2spthonot0  26398  el2wlkonotot  26400  el2wlkonotot1  26401  el2wlksotot  26409  usg2wlkonot  26410  2pthwlkonot  26412  usg2spthonot  26415  usg2spthonot0  26416  isrusgusrg  26459  isrusgusrgcl  26460  rusgranumwlks  26483  frgrancvvdeqlemC  26566  frgraeu  26581  frg2woteq  26587  frgrareggt1  26643  frgrareg  26644  frgraregord13  26646  ubthlem1  27110  norm-i  27370  hoeq  28003  nmopgt0  28155  pjimai  28419  chirredi  28637  addltmulALT  28689  sbcies  28706  iunrdx  28764  disjrdx  28786  cnvoprab  28886  archiabl  29083  oms0  29686  eulerpartgbij  29761  sgnneg  29929  sgn3da  29930  mrsubrn  30664  nofulllem2  31102  topfne  31519  unbdqndv1  31669  bj-hbntbi  31882  bj-abbi1dv  31969  bj-issetwt  32053  topdifinfeq  32374  wl-sb6rft  32509  wl-sbalnae  32524  sin2h  32569  poimirlem16  32595  poimirlem17  32596  poimirlem25  32604  mbfresfi  32626  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  ftc1anclem1  32655  isidlc  32984  elimhyps  33265  islshpsm  33285  lshpkrlem1  33415  opcon1b  33503  lautlt  34395  lauteq  34399  idlaut  34400  diblsmopel  35478  doch11  35680  istopclsd  36281  eqrabdioph  36359  rexzrexnn0  36386  zindbi  36529  expdiophlem2  36607  inintabd  36904  cnvcnvintabd  36925  cnvintabd  36928  fsovrfovd  37323  ntrclsiso  37385  ntrneifv3  37400  ntrneineine0lem  37401  ntrneicls11  37408  suprleubrd  37488  suprlubrd  37492  lemuldiv4d  37495  pm14.122a  37645  3impexpbicomi  37707  onfrALTlem5  37778  bitr3VD  38106  onfrALTlem5VD  38143  csbrngVD  38154  pwpwuni  38250  mapsnd  38383  supxrre3  38482  xrralrecnnge  38554  eliooshift  38576  smfrec  39674  2reu4a  39838  ralbinrald  39848  afvco2  39905  31prm  40050  dfeven3  40108  iseven5  40114  0noddALTV  40138  2noddALTV  40142  sgoldbaltlem1  40201  bgoldbtbndlem2  40222  pfxsuffeqwrdeq  40269  pfxccat3  40289  riotaeqimp  40338  subsubelfzo0  40359  usgredg2v  40454  edg0usgr  40479  usgr1v0edg  40483  dfnbgr2  40561  nbuhgr  40565  nbusgredgeu0  40596  nb3grprlem1  40608  nb3grpr  40610  uvtx2vtx1edgb  40626  upgrewlkle2  40808  1wlkeq  40838  red1wlk  40881  uhgr1wlkspthlem2  40960  usgr2wlkspth  40965  pthdlem1  40972  crctcsh1wlkn0lem1  41013  crctcsh1wlkn0lem4  41016  crctcsh  41027  iswwlksnx  41042  1wlkiswwlksupgr2  41074  wwlksm1edg  41078  wwlksnextsur  41106  wwlksnextproplem3  41117  wwlksnwwlksnon  41121  21wlkdlem4  41135  21wlkdlem5  41136  2pthdlem1  41137  s3wwlks2on  41160  wpthswwlks2on  41164  usgr2wspthons3  41167  elwspths2spth  41171  rusgrnumwwlks  41177  isclwwlksnx  41197  clwlkclwwlklem2a4  41206  clwlkclwwlk  41211  umgrclwwlksge2  41219  clwwisshclwws  41235  eclclwwlksn1  41259  clwlksfoclwwlk  41270  clwwlksnun  41281  31wlkdlem6  41332  frgrncvvdeqlemC  41478  frgreu  41491  av-clwwlkextfrlem1  41509  av-extwwlkfab  41520  av-frgrareggt1  41547  0nodd  41600  2nodd  41602  isassintop  41636  rnghmf1o  41693  isrngim  41694  uzlidlring  41719  funcringcsetcALTV2lem8  41835  funcringcsetclem8ALTV  41858  nn0sumltlt  41921  ply1mulgsumlem2  41969  islindeps  42036  lindslinindsimp1  42040  lindslinindsimp2  42046  snlindsntor  42054  zlmodzxznm  42080  ldepslinc  42092  difmodm1lt  42111  elbigo2  42144  elbigolo1  42149  logblt1b  42156  fldivexpfllog2  42157  nnolog2flm1  42182  digexp  42199  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator