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

Theorem bicomd 214
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 213 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 209 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  impbid2  217  syl5ibr  237  ibir  259  bitr2d  271  bitr3d  272  bitr4d  273  syl5rbb  275  syl6rbb  279  con1bid  346  pm5.5  352  imnot  356  baibr  528  rbaib  530  baibd  531  rbaibd  532  anabs5  645  annotanannot  854  pm5.55  962  pm5.54  1032  ninba  1036  pm5.75  1044  sbequ12r  2282  cbvalv  2448  sbal1  2622  euor2  2677  abbi1dv  2926  necon3bbid  3014  necon4bbid  3018  ralcom2  3291  rabrabi  3389  gencbvex  3443  sbhypf  3446  alexeqg  3525  clel2g  3532  clel3g  3534  reu8  3597  sbceq2a  3642  sbcco2  3654  reu8nf  3708  raltpd  4501  ssdifsn  4506  disjxun  4838  opabid  5174  soeq2  5249  posn  5386  xpiindi  5456  fvopab6  6529  cbvfo  6765  f1eqcocnv  6777  isoid  6800  isoini  6809  isosolem  6818  riotaeqimp  6855  resoprab2  6984  tfisi  7285  tfinds2  7290  f1oweALT  7379  dfoprab3  7453  opiota  7458  mpt2curryd  7627  oalimcl  7874  omword  7884  oeword  7904  nnacan  7942  nnmcan  7948  mapsnd  8131  findcard2s  8437  funisfsupp  8516  suppeqfsuppbi  8525  eqinf  8626  inflb  8631  infglb  8632  infglbb  8633  infltoreq  8644  infempty  8648  brwdomn0  8710  cantnfp1lem3  8821  ssrankr1  8942  r1pw  8952  djulf1o  9018  djurf1o  9019  aleph11  9187  alephval3  9213  gch-kn  9781  wunex2  9842  lttri2  10402  wloglei  10842  divne0b  10978  lemul1  11157  nnnle0  11333  div4p1lem1div2  11550  nn0ind-raph  11739  zindd  11740  suprfinzcl  11754  rebtwnz  12002  qreccl  12023  xrlttri2  12187  2resupmax  12233  xmulneg1  12313  iooshf  12466  difreicc  12523  fzofzim  12735  elfzomelpfzo  12792  elfznelfzo  12793  divfl0  12845  zmodid2  12918  2submod  12951  modfzo0difsn  12962  om2uzlti  12969  expcan  13132  hashvnfin  13365  hashneq0  13369  prhash2ex  13400  hashgt0elex  13402  hashgt12el  13423  hashgt12el2  13424  hashbclem  13449  hashf1lem2  13453  prprrab  13468  swrdn0  13650  swrd0  13654  2swrdeqwrdeq  13673  swrdswrd  13680  swrdccat3  13712  repswswrd  13751  cshf1  13776  cshw1repsw  13789  relexpindlem  14022  absz  14270  iserex  14606  prodrb  14879  absdvdsb  15219  dvdsabsb  15220  modmulconst  15232  dvdsadd  15243  dvdsabseq  15254  mod2eq0even  15286  oddnn02np1  15288  oddge22np1  15289  evennn02n  15290  evennn2n  15291  zeo5  15296  sadadd2lem2  15387  smupvallem  15420  gcdass  15479  lcmdvds  15536  lcmass  15542  divgcdcoprm0  15593  divgcdcoprmex  15594  1nprm  15606  dvdsnprmd  15617  ncoprmlnprm  15649  isevengcd2  15651  m1dvdsndvds  15716  cshws0  16016  sbcie2s  16123  sbcie3s  16124  dfiso2  16632  initoid  16855  termoid  16856  funcestrcsetclem8  16988  lublecllem  17189  odudlatb  17397  issubm2  17549  mgm2nsgrplem2  17607  nsgacs  17828  cycsubg2  17829  gapm  17936  sscntz  17956  pgrpsubgsymgbi  18024  f1omvdcnv  18061  pmtrprfvalrn  18105  odval2  18167  lsmcntz  18289  rhmf1o  18932  isrim  18933  snifpsrbag  19571  gsumply1eq  19879  dfprm2  20046  psgnfix2  20149  islinds3  20379  islindf4  20383  mdetdiaglem  20611  mdetunilem9  20633  slesolinv  20694  slesolex  20696  cpmatel2  20727  m2cpmghm  20758  m2cpminvid2  20769  pm2mpf1  20813  chfacfscmul0  20872  chfacfscmulfsupp  20873  chfacfpmmul0  20876  chfacfpmmulfsupp  20877  isopn2  21046  cmpsub  21413  connsub  21434  ncvs1  23165  rrxmvallem  23395  itg1mulc  23681  lhop1  23987  mdegleb  24034  lawcos  24756  leibpi  24879  2lgslem1a  25326  iscgra  25911  colinearalg  26000  edg0iedg0  26159  edg0iedg0OLD  26160  uhgreq12g  26170  uhgrvtxedgiedgb  26241  uhgrvtxedgiedgbOLD  26242  usgredg2v  26330  edg0usgr  26357  dfnbgr2  26442  nbuhgr  26451  nbusgredgeu0  26482  nb3grprlem1  26494  nb3grpr  26496  uvtx2vtx1edgb  26518  upgrewlkle2  26726  wlkeq  26753  redwlk  26793  uhgrwkspthlem2  26874  usgr2wlkspth  26879  pthdlem1  26886  cyclnspth  26920  crctcshwlkn0lem1  26927  crctcshwlkn0lem4  26930  crctcsh  26941  iswwlksnx  26957  wlkiswwlksupgr2  27000  wwlksm1edg  27004  wwlksnextsur  27033  wwlksnextproplem3  27045  wwlksnwwlksnonOLD  27051  2wlkdlem4  27064  2wlkdlem5  27065  2pthdlem1  27066  s3wwlks2on  27093  wpthswwlks2on  27098  wpthswwlks2onOLD  27099  elwspths2spth  27105  rusgrnumwwlks  27112  umgrclwwlkge2  27130  clwlkclwwlklem2a4  27136  clwlkclwwlk  27141  clwlkclwwlkflem  27143  clwwisshclwws  27154  isclwwlknx  27180  clwwlknwwlksnb  27201  eclclwwlkn1  27222  clwlksfoclwwlkOLD  27233  clwwlknonel  27258  clwwlknun  27277  clwwlknunOLD  27282  3wlkdlem6  27334  frgrncvvdeqlem9  27478  fusgreg2wsp  27507  numclwwlk2lem1lem  27514  numclwwlk2lem1lemOLD  27515  extwwlkfab  27527  frgrreggt1  27577  ubthlem1  28051  norm-i  28311  hoeq  28944  nmopgt0  29096  pjimai  29360  chirredi  29578  addltmulALT  29630  sbcies  29647  iunrdx  29704  disjrdx  29726  cnvoprabOLD  29822  archiabl  30074  oms0  30681  eulerpartgbij  30756  sgnneg  30924  sgn3da  30925  reprinrn  31018  mrsubrn  31730  sotrine  31977  etasslt  32238  topfne  32667  unbdqndv1  32813  bj-hbntbi  33007  bj-abbi1dv  33092  bj-issetwt  33164  dfgcd3  33484  topdifinfeq  33511  wl-sb6rft  33642  wl-sbalnae  33656  sin2h  33709  poimirlem16  33735  poimirlem17  33736  poimirlem25  33744  mbfresfi  33765  itg2addnclem  33770  itg2addnclem2  33771  itg2addnclem3  33772  ftc1anclem1  33794  isidlc  34122  islshpsm  34757  lshpkrlem1  34887  opcon1b  34975  lautlt  35868  lauteq  35872  idlaut  35873  diblsmopel  36949  doch11  37151  istopclsd  37762  eqrabdioph  37840  rexzrexnn0  37867  zindbi  38009  expdiophlem2  38087  inintabd  38382  cnvcnvintabd  38403  cnvintabd  38406  fsovrfovd  38800  ntrclsiso  38862  ntrneifv3  38877  ntrneineine0lem  38878  ntrneicls11  38885  suprleubrd  38963  suprlubrd  38967  lemuldiv4d  38970  pm14.122a  39119  3impexpbicomi  39181  onfrALTlem5  39252  bitr3VD  39575  onfrALTlem5VD  39612  csbrngVD  39623  pwpwuni  39715  supxrre3  40018  xrralrecnnge  40089  eliooshift  40210  limsupre2lem  40433  liminflimsupclim  40516  xlimbr  40530  smfrec  41475  2reu4a  41698  ralbinrald  41708  afvco2  41762  dfatdmfcoafv2  41840  subsubelfzo0  41908  pfxsuffeqwrdeq  41978  pfxccat3  41998  31prm  42084  dfeven3  42142  iseven5  42148  0noddALTV  42172  2noddALTV  42176  sbgoldbaltlem1  42239  bgoldbtbndlem2  42266  sprvalpwle2  42304  sprsymrelf1lem  42306  0nodd  42375  2nodd  42377  isassintop  42411  rnghmf1o  42468  isrngim  42469  uzlidlring  42494  funcringcsetcALTV2lem8  42608  funcringcsetclem8ALTV  42631  nn0sumltlt  42693  ply1mulgsumlem2  42740  islindeps  42807  lindslinindsimp1  42811  lindslinindsimp2  42817  snlindsntor  42825  zlmodzxznm  42851  ldepslinc  42863  difmodm1lt  42882  elbigo2  42911  elbigolo1  42916  logblt1b  42923  fldivexpfllog2  42924  nnolog2flm1  42949  digexp  42966  nn0sumshdiglemB  42979
  Copyright terms: Public domain W3C validator