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

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
StepHypRef Expression
1 bicomd.1 . 2 (𝜑 → (𝜓𝜒))
2 bicom 225 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 221 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  impbid2  229  syl5ibr  249  ibir  271  bitr2d  283  bitr3d  284  bitr4d  285  syl5rbb  287  syl6rbb  291  con1bid  359  pm5.5  365  imnot  369  baibr  540  rbaib  542  baibd  543  anabs5  662  annotanannot  833  pm5.55  946  pm5.54  1015  ninba  1019  pm5.75  1026  norassOLD  1535  sbequ12r  2253  cbvalvOLD  2412  sbal1  2551  euor2  2677  abbi1dv  2931  necon3bbid  3027  necon4bbid  3031  ralanid  3139  rexanid  3218  ralcom2  3319  sbralie  3421  gencbvex  3500  sbhypf  3503  alexeqg  3595  clel2g  3603  clel3g  3605  reu8  3675  sbceq2a  3735  sbcco2  3750  reu8nf  3809  2reu4lem  4426  reurexprg  4603  raltpd  4680  ssdifsn  4684  disjxun  5031  opabidw  5380  opabid  5381  soeq2  5463  posn  5605  xpiindi  5674  dmopab2rex  5754  fvopab6  6782  cbvfo  7027  f1eqcocnv  7039  f1eqcocnvOLD  7040  isoid  7065  isoini  7074  isosolem  7083  riotaeqimp  7123  resoprab2  7254  tfisi  7557  tfinds2  7562  f1oweALT  7659  dfoprab3  7738  opiota  7743  mpocurryd  7922  oalimcl  8173  omword  8183  oeword  8203  nnacan  8241  nnmcan  8247  mapsnd  8437  findcard2s  8747  funisfsupp  8826  suppeqfsuppbi  8835  eqinf  8936  inflb  8941  infglb  8942  infglbb  8943  infltoreq  8954  infempty  8959  brwdomn0  9021  cantnfp1lem3  9131  ssrankr1  9252  r1pw  9262  djulf1o  9329  djurf1o  9330  aleph11  9499  alephval3  9525  gch-kn  10092  wunex2  10153  lttri2  10716  wloglei  11165  divne0b  11302  lemul1  11485  nnnle0  11662  div4p1lem1div2  11884  nn0ind-raph  12074  zindd  12075  suprfinzcl  12089  rebtwnz  12339  qreccl  12360  elpq  12366  xrlttri2  12527  2resupmax  12573  xmulneg1  12654  iooshf  12808  difreicc  12866  fzofzim  13083  elfzomelpfzo  13140  elfznelfzo  13141  zmodid2  13266  2submod  13299  modfzo0difsn  13310  om2uzlti  13317  expcan  13533  hashvnfin  13721  hashneq0  13725  prhash2ex  13760  hashgt0elex  13762  hashgt12el  13783  hashgt12el2  13784  hashbclem  13810  hashf1lem2  13814  prprrab  13831  swrd0  14015  pfxn0  14043  swrdswrd  14062  pfxccat3  14091  repswswrd  14141  cshf1  14167  cshw1repsw  14180  relexpindlem  14418  absz  14667  iserex  15009  prodrb  15282  absdvdsb  15624  dvdsabsb  15625  modmulconst  15637  dvdsadd  15648  dvdsabseq  15659  mod2eq0even  15691  oddnn02np1  15693  oddge22np1  15694  evennn02n  15695  evennn2n  15696  zeo5  15701  sadadd2lem2  15793  smupvallem  15826  gcdass  15889  lcmdvds  15946  lcmass  15952  divgcdcoprm0  16003  divgcdcoprmex  16004  1nprm  16017  dvdsnprmd  16028  ncoprmlnprm  16062  isevengcd2  16064  m1dvdsndvds  16129  cshws0  16431  sbcie2s  16536  sbcie3s  16537  dfiso2  17038  initoid  17261  termoid  17262  funcestrcsetclem8  17393  lublecllem  17594  odudlatb  17802  issubm2  17965  mgm2nsgrplem2  18080  nsgacs  18310  cycsubg2  18349  gapm  18432  sscntz  18452  pgrpsubgsymgbi  18532  f1omvdcnv  18568  pmtrprfvalrn  18612  odval2  18675  lsmcntz  18801  rhmf1o  19484  isrim  19485  dfprm2  20191  psgnfix2  20292  islinds3  20527  islindf4  20531  snifpsrbag  20608  gsumply1eq  20938  mdetdiaglem  21207  mdetunilem9  21229  slesolinv  21289  slesolex  21291  cpmatel2  21322  m2cpmghm  21353  m2cpminvid2  21364  pm2mpf1  21408  chfacfscmul0  21467  chfacfscmulfsupp  21468  chfacfpmmul0  21471  chfacfpmmulfsupp  21472  isopn2  21641  cmpsub  22009  connsub  22030  ncvs1  23766  rrxmvallem  24012  itg1mulc  24312  lhop1  24621  mdegleb  24669  lawcos  25406  leibpi  25532  2lgslem1a  25979  2sq2  26021  iscgra  26607  colinearalg  26708  edg0iedg0  26852  uhgreq12g  26862  uhgrvtxedgiedgb  26933  usgredg2v  27021  edg0usgr  27047  dfnbgr2  27131  nbuhgr  27137  nbusgredgeu0  27162  nb3grprlem1  27174  nb3grpr  27176  uvtx2vtx1edgb  27193  redwlk  27466  uhgrwkspthlem2  27547  usgr2wlkspth  27552  pthdlem1  27559  cyclnspth  27593  crctcshwlkn0lem1  27600  crctcshwlkn0lem4  27603  crctcsh  27614  iswwlksnx  27630  wwlksm1edg  27671  wwlksnextsurj  27690  wwlksnextproplem3  27701  2wlkdlem4  27718  2wlkdlem5  27719  2pthdlem1  27720  s3wwlks2on  27746  wpthswwlks2on  27751  elwspths2spth  27757  rusgrnumwwlks  27764  umgrclwwlkge2  27780  clwlkclwwlklem2a4  27786  clwlkclwwlk  27791  clwlkclwwlkflem  27793  clwwisshclwws  27804  isclwwlknx  27825  clwwlknwwlksnb  27844  eclclwwlkn1  27864  clwwlknonel  27884  clwwlknun  27901  3wlkdlem6  27954  frgrncvvdeqlem9  28096  fusgreg2wsp  28125  numclwwlk2lem1lem  28131  extwwlkfab  28141  frgrreggt1  28182  ubthlem1  28657  norm-i  28916  hoeq  29547  nmopgt0  29699  pjimai  29963  chirredi  30181  addltmulALT  30233  opreu2reuALT  30251  sbcies  30262  rmounid  30270  iunrdx  30331  disjrdx  30358  cnvoprabOLD  30486  archiabl  30881  ist0cld  31190  oms0  31669  eulerpartgbij  31744  sgnneg  31912  sgn3da  31913  reprinrn  32003  usgrgt2cycl  32491  satfv1lem  32723  satf0op  32738  dmopab3rexdif  32766  satefvfmla0  32779  mrsubrn  32874  sotrine  33117  etasslt  33388  topfne  33816  unbdqndv1  33961  bj-hbntbi  34152  bj-issetwt  34314  copsex2d  34555  bj-elid6  34586  dfgcd3  34739  topdifinfeq  34768  wl-sb6rft  34948  wl-sbalnae  34962  wl-dfralf  35003  sin2h  35046  poimirlem16  35072  poimirlem17  35073  poimirlem25  35081  mbfresfi  35102  itg2addnclem  35107  itg2addnclem2  35108  itg2addnclem3  35109  ftc1anclem1  35129  isidlc  35452  islshpsm  36275  lshpkrlem1  36405  opcon1b  36493  lautlt  37386  lauteq  37390  idlaut  37391  diblsmopel  38466  doch11  38668  recbothd  39279  metakunt16  39362  rabeqcda  39395  prjsprellsp  39602  prjspeclsp  39603  istopclsd  39638  eqrabdioph  39715  rexzrexnn0  39742  zindbi  39884  expdiophlem2  39960  infordmin  40237  inintabd  40276  cnvcnvintabd  40297  cnvintabd  40300  sqrtcvallem1  40328  reabsifneg  40329  fsovrfovd  40707  ntrclsiso  40767  ntrneifv3  40782  ntrneineine0lem  40783  ntrneicls11  40790  suprleubrd  40867  suprlubrd  40870  lemuldiv4d  40873  pm14.122a  41123  3impexpbicomi  41183  onfrALTlem5  41245  bitr3VD  41552  onfrALTlem5VD  41588  csbrngVD  41599  pwpwuni  41688  supxrre3  41954  xrralrecnnge  42023  eliooshift  42140  limsupre2lem  42363  liminflimsupclim  42446  xlimbr  42466  smfrec  43418  reuf1odnf  43660  2reuimp  43668  ralbinrald  43675  afvco2  43729  dfatdmfcoafv2  43807  recnmulnred  43859  sqrtnegnre  43861  subsubelfzo0  43880  ichcircshi  43968  sprvalpwle2  44003  sprsymrelf1lem  44005  sbcpr  44035  poprelb  44038  31prm  44111  requad01  44136  dfeven3  44173  iseven5  44179  0noddALTV  44204  2noddALTV  44208  fpprmod  44242  sbgoldbaltlem1  44294  bgoldbtbndlem2  44321  isomuspgrlem2d  44346  0nodd  44427  2nodd  44429  isassintop  44467  rnghmf1o  44524  isrngim  44525  uzlidlring  44550  funcringcsetcALTV2lem8  44664  funcringcsetclem8ALTV  44687  nn0sumltlt  44749  ply1mulgsumlem2  44792  islindeps  44859  lindslinindsimp1  44863  lindslinindsimp2  44869  snlindsntor  44877  zlmodzxznm  44903  ldepslinc  44915  difmodm1lt  44933  elbigo2  44963  elbigolo1  44968  logblt1b  44975  fldivexpfllog2  44976  nnolog2flm1  45001  digexp  45018  nn0sumshdiglemB  45031  itsclquadeu  45188  itscnhlinecirc02p  45196
  Copyright terms: Public domain W3C validator