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

Theorem bicomd 224
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 223 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 219 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  impbid2  227  syl5ibr  247  ibir  269  bitr2d  281  bitr3d  282  bitr4d  283  syl5rbb  285  syl6rbb  289  con1bid  357  pm5.5  363  imnot  367  baibr  537  rbaib  539  baibd  540  anabs5  659  annotanannot  830  pm5.55  942  pm5.54  1011  ninba  1015  pm5.75  1022  norassOLD  1525  sbequ12r  2245  cbvalvOLD  2414  sbal1  2568  euor2  2693  abbi1dv  2952  necon3bbid  3053  necon4bbid  3057  ralanid  3168  rexanid  3252  ralcom2w  3363  ralcom2  3364  sbralie  3472  gencbvex  3550  sbhypf  3553  alexeqg  3643  clel2g  3651  clel3g  3653  reu8  3723  sbceq2a  3783  sbcco2  3798  reu8nf  3859  2reu4lem  4463  reurexprg  4634  raltpd  4710  ssdifsn  4714  disjxun  5056  opabidw  5404  opabid  5405  soeq2  5489  posn  5631  xpiindi  5700  dmopab2rex  5780  fvopab6  6794  cbvfo  7036  f1eqcocnv  7048  isoid  7071  isoini  7080  isosolem  7089  riotaeqimp  7129  resoprab2  7260  tfisi  7561  tfinds2  7566  f1oweALT  7664  dfoprab3  7743  opiota  7748  mpocurryd  7926  oalimcl  8176  omword  8186  oeword  8206  nnacan  8244  nnmcan  8250  mapsnd  8439  findcard2s  8748  funisfsupp  8827  suppeqfsuppbi  8836  eqinf  8937  inflb  8942  infglb  8943  infglbb  8944  infltoreq  8955  infempty  8960  brwdomn0  9022  cantnfp1lem3  9132  ssrankr1  9253  r1pw  9263  djulf1o  9330  djurf1o  9331  aleph11  9499  alephval3  9525  gch-kn  10088  wunex2  10149  lttri2  10712  wloglei  11161  divne0b  11298  lemul1  11481  nnnle0  11659  div4p1lem1div2  11881  nn0ind-raph  12071  zindd  12072  suprfinzcl  12086  rebtwnz  12336  qreccl  12358  elpq  12364  xrlttri2  12525  2resupmax  12571  xmulneg1  12652  iooshf  12805  difreicc  12860  fzofzim  13074  elfzomelpfzo  13131  elfznelfzo  13132  zmodid2  13257  2submod  13290  modfzo0difsn  13301  om2uzlti  13308  expcan  13523  hashvnfin  13711  hashneq0  13715  prhash2ex  13750  hashgt0elex  13752  hashgt12el  13773  hashgt12el2  13774  hashbclem  13800  hashf1lem2  13804  prprrab  13821  swrd0  14010  pfxn0  14038  swrdswrd  14057  pfxccat3  14086  repswswrd  14136  cshf1  14162  cshw1repsw  14175  relexpindlem  14412  absz  14661  iserex  15003  prodrb  15276  absdvdsb  15618  dvdsabsb  15619  modmulconst  15631  dvdsadd  15642  dvdsabseq  15653  mod2eq0even  15685  oddnn02np1  15687  oddge22np1  15688  evennn02n  15689  evennn2n  15690  zeo5  15695  sadadd2lem2  15789  smupvallem  15822  gcdass  15885  lcmdvds  15942  lcmass  15948  divgcdcoprm0  15999  divgcdcoprmex  16000  1nprm  16013  dvdsnprmd  16024  ncoprmlnprm  16058  isevengcd2  16060  m1dvdsndvds  16125  cshws0  16425  sbcie2s  16530  sbcie3s  16531  dfiso2  17032  initoid  17255  termoid  17256  funcestrcsetclem8  17387  lublecllem  17588  odudlatb  17796  issubm2  17959  mgm2nsgrplem2  18024  nsgacs  18254  cycsubg2  18293  gapm  18376  sscntz  18396  pgrpsubgsymgbi  18467  f1omvdcnv  18503  pmtrprfvalrn  18547  odval2  18610  lsmcntz  18736  rhmf1o  19415  isrim  19416  snifpsrbag  20076  gsumply1eq  20403  dfprm2  20571  psgnfix2  20673  islinds3  20908  islindf4  20912  mdetdiaglem  21137  mdetunilem9  21159  slesolinv  21219  slesolex  21221  cpmatel2  21251  m2cpmghm  21282  m2cpminvid2  21293  pm2mpf1  21337  chfacfscmul0  21396  chfacfscmulfsupp  21397  chfacfpmmul0  21400  chfacfpmmulfsupp  21401  isopn2  21570  cmpsub  21938  connsub  21959  ncvs1  23690  rrxmvallem  23936  itg1mulc  24234  lhop1  24540  mdegleb  24587  lawcos  25321  leibpi  25448  2lgslem1a  25895  2sq2  25937  iscgra  26523  colinearalg  26624  edg0iedg0  26768  uhgreq12g  26778  uhgrvtxedgiedgb  26849  usgredg2v  26937  edg0usgr  26963  dfnbgr2  27047  nbuhgr  27053  nbusgredgeu0  27078  nb3grprlem1  27090  nb3grpr  27092  uvtx2vtx1edgb  27109  redwlk  27382  uhgrwkspthlem2  27463  usgr2wlkspth  27468  pthdlem1  27475  cyclnspth  27509  crctcshwlkn0lem1  27516  crctcshwlkn0lem4  27519  crctcsh  27530  iswwlksnx  27546  wwlksm1edg  27587  wwlksnextsurj  27606  wwlksnextproplem3  27618  2wlkdlem4  27635  2wlkdlem5  27636  2pthdlem1  27637  s3wwlks2on  27663  wpthswwlks2on  27668  elwspths2spth  27674  rusgrnumwwlks  27681  umgrclwwlkge2  27697  clwlkclwwlklem2a4  27703  clwlkclwwlk  27708  clwlkclwwlkflem  27710  clwwisshclwws  27721  isclwwlknx  27742  clwwlknwwlksnb  27762  eclclwwlkn1  27782  clwwlknonel  27802  clwwlknun  27819  3wlkdlem6  27872  frgrncvvdeqlem9  28014  fusgreg2wsp  28043  numclwwlk2lem1lem  28049  extwwlkfab  28059  frgrreggt1  28100  ubthlem1  28575  norm-i  28834  hoeq  29465  nmopgt0  29617  pjimai  29881  chirredi  30099  addltmulALT  30151  opreu2reuALT  30168  sbcies  30179  rmounid  30187  iunrdx  30244  disjrdx  30270  cnvoprabOLD  30383  archiabl  30755  oms0  31455  eulerpartgbij  31530  sgnneg  31698  sgn3da  31699  reprinrn  31789  usgrgt2cycl  32275  satfv1lem  32507  satf0op  32522  dmopab3rexdif  32550  satefvfmla0  32563  mrsubrn  32658  sotrine  32901  etasslt  33172  topfne  33600  unbdqndv1  33745  bj-hbntbi  33936  bj-issetwt  34087  copsex2d  34324  bj-elid6  34355  dfgcd3  34488  topdifinfeq  34514  wl-sb6rft  34666  wl-sbalnae  34680  wl-dfralf  34721  sin2h  34764  poimirlem16  34790  poimirlem17  34791  poimirlem25  34799  mbfresfi  34820  itg2addnclem  34825  itg2addnclem2  34826  itg2addnclem3  34827  ftc1anclem1  34849  isidlc  35176  islshpsm  35998  lshpkrlem1  36128  opcon1b  36216  lautlt  37109  lauteq  37113  idlaut  37114  diblsmopel  38189  doch11  38391  rabeqcda  38986  prjsprellsp  39141  prjspeclsp  39142  istopclsd  39177  eqrabdioph  39254  rexzrexnn0  39281  zindbi  39423  expdiophlem2  39499  infordmin  39779  inintabd  39819  cnvcnvintabd  39840  cnvintabd  39843  fsovrfovd  40235  ntrclsiso  40297  ntrneifv3  40312  ntrneineine0lem  40313  ntrneicls11  40320  suprleubrd  40397  suprlubrd  40401  lemuldiv4d  40404  pm14.122a  40634  3impexpbicomi  40694  onfrALTlem5  40756  bitr3VD  41063  onfrALTlem5VD  41099  csbrngVD  41110  pwpwuni  41199  supxrre3  41473  xrralrecnnge  41542  eliooshift  41662  limsupre2lem  41885  liminflimsupclim  41968  xlimbr  41988  smfrec  42945  reuf1odnf  43187  2reuimp  43195  ralbinrald  43202  afvco2  43256  dfatdmfcoafv2  43334  recnmulnred  43386  sqrtnegnre  43388  subsubelfzo0  43407  ichcircshi  43459  sprvalpwle2  43498  sprsymrelf1lem  43500  sbcpr  43530  poprelb  43533  31prm  43607  requad01  43633  dfeven3  43670  iseven5  43676  0noddALTV  43701  2noddALTV  43705  fpprmod  43739  sbgoldbaltlem1  43791  bgoldbtbndlem2  43818  isomuspgrlem2d  43843  0nodd  43924  2nodd  43926  isassintop  44015  rnghmf1o  44072  isrngim  44073  uzlidlring  44098  funcringcsetcALTV2lem8  44212  funcringcsetclem8ALTV  44235  nn0sumltlt  44296  ply1mulgsumlem2  44339  islindeps  44406  lindslinindsimp1  44410  lindslinindsimp2  44416  snlindsntor  44424  zlmodzxznm  44450  ldepslinc  44462  difmodm1lt  44480  elbigo2  44510  elbigolo1  44515  logblt1b  44522  fldivexpfllog2  44523  nnolog2flm1  44548  digexp  44565  nn0sumshdiglemB  44578  itsclquadeu  44662  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator