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

Theorem impcom 437
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
impcom  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 31 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 436 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  mpan9  477  bianir  978  19.29r  1744  19.41v  1838  equtr2  1877  19.41  2070  nfsb4t  2238  2euex  2393  gencl  3063  2gencl  3064  vtocl4g  3104  rspccva  3135  sseq0  3769  minel  3824  r19.2z  3849  elelpwi  3953  eqoreldif  4004  elpreqpr  4153  ssuni  4212  disji2  4382  invdisjrab  4385  disjiun  4386  trint0  4507  ssexg  4542  pofun  4776  solin  4783  2optocl  4917  3optocl  4918  elrnmpt1  5089  resieq  5121  funimaexg  5670  fnun  5692  fss  5749  fun  5758  fvelimab  5936  fvmptss  5973  fvn0ssdmfun  6028  fvcofneq  6045  fmptco  6072  fnressn  6092  fressnfv  6094  fvn0fvelrn  6097  fmptsng  6101  fvtp2g  6131  fvtp3g  6132  tpres  6133  fnex  6148  funfvima3  6160  isores3  6244  dmfex  6770  f1o2ndf1  6923  frxp  6925  fnse  6932  ressuppssdif  6955  funsssuppss  6960  suppss  6964  mpt2xopxnop0  6980  reldmtpos  6999  wfrfun  7064  wfrlem12  7065  smores  7089  tfrlem7  7119  tz7.48-2  7177  tz7.49  7180  oacl  7255  omcl  7256  oecl  7257  oarec  7281  oewordri  7311  oeworde  7312  oelim2  7314  oeoa  7316  oeoelem  7317  oeoe  7318  nnacl  7330  nnmcl  7331  nnecl  7332  nnmsucr  7344  2ecoptocl  7472  undifixp  7576  ssct  7671  xpf1o  7752  limensuc  7767  ac6sfi  7833  frfi  7834  difinf  7859  f1dmvrnfibi  7876  f1vrnfibi  7877  suppeqfsuppbi  7915  elfiun  7962  dffi3  7963  xpwdomg  8118  preleq  8140  infdiffi  8181  epfrs  8233  rankxpsuc  8371  tskwe  8402  infxpenlem  8462  fseqenlem1  8473  kmlem2  8599  cff1  8706  cflim2  8711  sornom  8725  infpssrlem4  8754  fin23lem26  8773  fin23lem30  8790  fin23lem34  8794  isf32lem11  8811  fin67  8843  isfin7-2  8844  fin1a2lem10  8857  axcc2lem  8884  axdc2lem  8896  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  iunfo  8982  tsk0  9206  gruina  9261  grur1a  9262  mulcanenq  9403  reclem2pr  9491  supsrlem  9553  supsr  9554  ax1rid  9603  negf1o  10070  mulgt1  10486  fiminre  10577  lbreu  10578  nnaddcl  10653  nnmulcl  10654  nn0n0n1ge2b  10957  nn0indd  11055  fzind  11056  fnn0ind  11057  uzaddcl  11238  uzinfi  11261  nn01to3  11280  xmulasslem2  11593  supxrunb1  11630  supxrunb2  11631  infmremnf  11658  infmrp1  11659  uzsubsubfz  11847  elfz1b  11890  elfz0ubfz0  11920  fz0fzdiffz0  11925  elfzmlbp  11927  fzofzim  11990  elfzom1elp1fzo  12010  elfzom1p1elfzo  12022  ssfzo12bi  12035  fzonfzoufzol  12043  elfznelfzob  12046  injresinjlem  12056  injresinj  12057  modaddmodup  12187  modfzo0difsn  12195  modsumfzodifsn  12196  addmodlteq  12198  om2uzlti  12202  fsequb  12226  ssnn0fi  12235  ser1const  12307  expcllem  12321  expeq0  12340  faclbnd  12513  faclbnd6  12522  hasheqf1oi  12572  hashf1rn  12573  hashgadd  12594  hashunx  12603  hashnn0n0nn  12608  hashgt0elex  12616  hashss  12624  hashxp  12647  hashimarni  12652  seqcoll  12668  hash2exprb  12673  hashge2el2difr  12679  elss2prb  12684  brfi1indlem  12690  fi1uzind  12691  brfi1indALT  12694  fi1uzindOLD  12697  brfi1indALTOLD  12700  lswlgt0cl  12767  swrdnd  12842  swrd0  12844  swrdsbslen  12858  swrdspsleq  12859  2swrd1eqwrdeq  12864  swrdswrdlem  12869  swrdswrd  12870  wrd2ind  12888  swrdccatfn  12892  swrdccatin1  12893  swrdccatin12lem2a  12895  swrdccatin2  12897  swrdccatin12lem2  12899  swrdccatin12lem3  12900  swrdccatin12  12901  swrdccat3  12902  swrdccat  12903  swrdccat3blem  12905  repswswrd  12941  repswrevw  12943  cshwmodn  12951  cshwsublen  12952  cshwidxmod  12959  cshwidxmodr  12960  cshf1  12966  2cshw  12969  cshweqrep  12977  cshw1  12978  2cshwcshw  12981  cshwcshid  12983  cshwcsh2id  12984  wrdlen2i  13093  2swrd2eqwrdeq  13103  wwlktovfo  13108  relexpsucnnl  13172  rtrclreclem3  13200  rtrclreclem4  13201  relexpindlem  13203  cjexp  13290  absexp  13444  r19.29uz  13490  caubnd  13498  sqreu  13500  climshft  13717  climub  13802  climserle  13803  sumss  13867  sumss2  13869  modfsummods  13930  o1fsum  13950  binom  13965  bcxmas  13970  climcndslem1  13984  climcndslem2  13985  cvgrat  14016  clim2prod  14021  prodfn0  14027  prodfrec  14028  ntrivcvgfvn0  14032  fprodn0  14110  fprodefsum  14226  demoivreALT  14332  znnenlem  14341  ruclem8  14366  dvdsfac  14438  smu01lem  14538  dvdslegcd  14557  gcdneg  14569  gcdmultiple  14597  seq1st  14609  alginv  14613  lcmf  14685  lcmftp  14688  lcmfunsnlem2lem2  14691  lcmfunsnlem  14693  lcmfun  14697  ncoprmgcdne1b  14734  prmdvdsexp  14746  ncoprmlnprm  14756  coprmproddvdslem  14758  coprmproddvds  14759  fvprmselgcd1  15082  prmgaplem6  15105  prmgaplem7  15106  prmgaplem8  15107  cshwshashlem1  15144  inveq  15757  catsubcat  15822  initoeu2lem0  15986  initoeu2lem1  15987  funcestrcsetclem8  16110  funcestrcsetclem9  16111  fthestrcsetc  16113  fullestrcsetc  16114  funcsetcestrclem9  16126  fthsetcestrc  16128  fullsetcestrc  16129  lubss  16445  lubel  16446  mgmb1mgm1  16577  frmdgsum  16724  mgm2nsgrplem3  16732  gaass  17029  gsumwrev  17095  symgextf1lem  17139  symgextf1  17140  fvcosymgeq  17148  gsmsymgreq  17151  symgfixelsi  17154  pmtrprfv3  17173  symggen  17189  pmtrprfval  17206  gsumzres  17621  gsumzunsnd  17666  srgmulgass  17842  srgbinom  17856  lmodvsmmulgdi  18204  0ringnnzr  18570  assamulgscm  18651  gsumply1subr  18904  gsummoncoe1  18975  pf1ind  19020  cnfldmulg  19077  cnfldexp  19078  psgndiflemB  19245  matmulcell  19547  mat1dimscm  19577  dmatmul  19599  dmatscmcl  19605  scmataddcl  19618  scmatsubcl  19619  scmatsgrp1  19624  mavmulsolcl  19653  ma1repveval  19673  1marepvmarrepid  19677  symgmatr01lem  19755  slesolvec  19781  cramerimplem2  19786  decpmatmullem  19872  pm2mpf1  19900  mp2pm2mplem4  19910  monmat2matmon  19925  chpscmat  19943  chpscmatgsumbin  19945  fvmptnn04ifb  19952  chfacfscmul0  19959  chfacfscmulgsum  19961  chfacfpmmul0  19963  chfacfpmmulgsum  19965  cpmadugsumlemF  19977  clsss  20146  ntrss  20147  restntr  20275  cmpsublem  20491  cmpsub  20492  2ndcrest  20546  txindislem  20725  t0kq  20910  filufint  21013  fbflim2  21070  flftg  21089  alexsubALTlem4  21143  cnextfvval  21158  tmdmulg  21185  ustuqtop4  21337  xmettri2  21433  mettri  21445  metss  21601  lmmbr  22306  caublcls  22356  lmcau  22360  ovolunlem1a  22527  nulmbl2  22568  voliunlem1  22582  iunmbl  22585  volsup  22588  dvlip  23024  dvfsumle  23052  degltlem1  23100  ply1divex  23166  plyco  23274  dgrnznn  23280  dvnply2  23319  plydivex  23329  aannenlem2  23364  aaliou3lem2  23378  ulmcau  23429  dchrisumlem1  24406  dchrisumlem2  24407  dchrisumlem3  24408  qabvle  24542  ostthlem2  24545  ostth2lem2  24551  axeuclidlem  25071  usgra2edg  25188  usgraedg4  25193  usgraidx2vlem2  25198  nbusgra  25235  nbgraf1olem5  25252  nb3graprlem1  25258  nb3graprlem2  25259  cusgrarn  25266  nbcusgra  25270  cusgrasize2inds  25284  sizeusglecusglem1  25291  uvtxnbgra  25300  iswlkg  25331  wlkn0  25334  usgrwlknloop  25372  redwlk  25415  wlkdvspthlem  25416  usgra2adedgwlkonALT  25423  usgra2wlkspthlem1  25426  usgra2wlkspthlem2  25427  usgra2wlkspth  25428  fargshiftf1  25444  usgrcyclnl1  25447  usgrcyclnl2  25448  nvnencycllem  25450  constr3trllem2  25458  wwlknimp  25494  wlkiswwlk1  25497  wlkiswwlk2  25504  wlklniswwlkn1  25506  wlklniswwlkn2  25507  vfwlkniswwlkn  25513  wwlknext  25531  wwlknredwwlkn  25533  wwlknredwwlkn0  25534  wwlkextfun  25536  wwlkextinj  25537  wwlkextsur  25538  wwlkextproplem3  25550  clwlkisclwwlklem2a1  25586  clwlkisclwwlklem2fv2  25590  clwlkisclwwlklem2a4  25591  clwlkisclwwlklem2a  25592  clwlkisclwwlklem1  25594  clwwlkel  25600  clwwlkf1  25603  clwwlkfo  25604  clwwlknwwlkncl  25607  clwwlkext2edg  25609  wwlkext2clwwlk  25610  wwlksubclwwlk  25611  clwwisshclwwlem  25613  clwwisshclww  25614  clwwisshclwwn  25615  erclwwlktr  25622  clwwlknscsh  25626  erclwwlkntr  25634  eleclclwwlkn  25640  hashecclwwlkn1  25641  usghashecclwwlk  25642  clwlkfclwwlk  25651  clwlkfoclwwlk  25652  el2wlkonot  25676  el2spthonot  25677  el2wlkonotot0  25679  usg2spthonot0  25696  rusgrasn  25752  rusgranumwlk  25764  clwlknclwlkdifs  25767  frgra1v  25805  1to2vfriswmgra  25813  1to3vfriswmgra  25814  3cyclfrgrarn1  25819  4cycl2vnunb  25824  frgrancvvdeqlem3  25839  frgrawopreglem3  25853  frgrawopreglem4  25854  frgrawopreg  25856  frg2woteqm  25866  2spotdisj  25868  2spotiundisj  25869  usg2spot2nb  25872  extwwlkfablem1  25881  clwwlkextfrlem1  25883  extwwlkfablem2  25885  numclwwlkun  25886  numclwwlkovf2ex  25893  numclwwlkovgelim  25896  numclwlk1lem2foa  25898  numclwlk1lem2f1  25901  numclwlk1lem2fo  25902  numclwwlk1  25905  numclwlk2lem2f  25910  numclwlk2lem2f1o  25912  numclwwlk5  25919  frgrareg  25924  frgraregord013  25925  friendship  25929  isgrpo  26005  opidonOLD  26131  grpomndo  26155  vcdi  26252  vcdir  26253  vcass  26254  nmosetre  26486  hlim2  26926  shscli  27051  chintcli  27065  dfch2  27141  spansncvi  27386  nmopsetretALT  27597  nmfnsetre  27611  lnopl  27648  lnfnl  27665  pjss2coi  27898  pjorthcoi  27903  pjscji  27904  pjssdif2i  27908  pjclem4a  27932  pj3lem1  27940  strlem5  27989  hstrlem5  27997  cvmdi  28058  mdslmd3i  28066  atcv1  28114  atcvat4i  28131  cdj3lem2a  28170  cdj3lem3a  28173  iuninc  28253  disji2f  28264  disjif2  28268  fmptcof2  28334  nnindd  28458  xrsmulgzz  28515  ofldchr  28651  esumfzf  28964  issgon  29019  voliune  29125  volfiniune  29126  rrvsum  29360  bnj228  29615  bnj1294  29701  bnj229  29767  bnj607  29799  bnj908  29814  bnj953  29822  bnj1118  29865  bnj1174  29884  bnj1388  29914  cvmliftlem15  30093  iprodefisumlem  30447  faclimlem1  30450  dfon2lem6  30505  tfisg  30528  poseq  30562  frrlem4  30588  frrlem5c  30591  frrlem11  30597  nodenselem5  30645  nocvxminlem  30650  nocvxmin  30651  idinside  30922  nn0prpw  31050  onsucconi  31168  exlimim  31814  exellim  31817  icoreclin  31830  wl-aleq  31938  fin2so  31996  poimirlem4  32008  poimirlem26  32030  itg2addnclem  32057  upixp  32120  welb  32127  sdclem2  32135  metf1o  32148  sstotbnd3  32172  isbndx  32178  ismtycnv  32198  heiborlem4  32210  bfplem1  32218  ax12eq  32576  ax12el  32577  cvrat4  33079  mzpexpmpt  35658  diophren  35727  expmordi  35866  rmxypos  35868  jm2.17a  35881  jm2.17b  35882  rmygeid  35885  divalgmodcl  35913  jm2.18  35914  jm2.25  35925  jm2.15nn0  35929  jm2.16nn0  35930  pwslnm  36023  isnumbasgrplem1  36031  dgraalem  36078  dgraalemOLD  36079  relexpiidm  36367  relexpmulnn  36372  relexpmulg  36373  relexp01min  36376  relexp0a  36379  relexpxpmin  36380  dvgrat  36731  radcnvrat  36733  sspwimpcf  37380  sspwimpcfVD  37381  e2ebindALT  37389  2reurex  38747  2reu1  38752  eu2ndop1stv  38768  afvfv0bi  38799  afveu  38800  afvres  38819  aovmpt4g  38848  ndmaovass  38853  ndmaovdistr  38854  nltle2tri  38861  smonoord  38863  fzopredsuc  38865  iccpartres  38877  iccpartiltu  38881  iccpartigtl  38882  iccpartgt  38886  icceuelpartlem  38894  gbegt5  39007  bgoldbwt  39023  nnsum3primesgbe  39032  wtgoldbnnsum4prm  39042  bgoldbnnsum3prm  39044  bgoldbtbndlem2  39046  bgoldbtbndlem3  39047  bgoldbtbndlem4  39048  bgoldbtbnd  39049  pfxsuff1eqwrdeq  39095  pfxccatin12lem2  39112  pfxccatin12  39113  pfxccat3  39114  pfxccat3a  39117  cshword2  39125  falseral0  39133  propeqop  39146  ssrelrn  39156  imarnf1pr  39162  funsndifnop  39168  subsubelfzo0  39207  fzoopth  39208  2ffzoeq  39209  incistruhgr  39325  umgredgprv  39352  umgrpredgav  39391  usgredgprvALT  39440  uhgr2edg  39453  usgredg2vlem2  39467  subgrfun  39517  umgrres1lem  39541  upgrres1  39544  fusgrfis  39560  uhgrnbgr0nb  39586  nbgr1vtx  39590  nb3grprlem1  39618  uvtxa01vtx0  39633  uvtx2vtx1edg  39635  cusgrsize2inds  39679  1hevtxdg1  39728  upgrewlkle2  39812  upgr1wlkwlk  39842  upgrwlkedg  39845  1wlkres  39866  red1wlk  39868  lfgr1wlknloop  39881  pthdadjvtx  39923  upgr2pthnlp  39925  upgrwlkdvdelem  39928  upgrwlkdvde  39929  uhgr1wlkspthlem2  39946  usgr2wlkneq  39948  pthdlem2lem  39953  lfgrn1cycl  39984  uspgrn2crct  39986  crctcsh1wlkn0lem3  39990  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem5  39992  is01wlklem  40006  upgr3v3e3cycl  40094  uhgr3cyclex  40096  upgr4cycl4dv4e  40099  upgreupthi  40121  eulerpath  40153  eucrctshift  40155  eucrct2eupth  40157  usgra2pthspth  40173  usgra2pth  40176  usgrauvtxvd  40180  usgpredgv  40219  usgpredgvALT  40220  usgedgvadf1lem2  40234  usgedgvadf1ALTlem2  40237  usgresvm1  40263  usgfis  40266  usgresvm1ALT  40267  usgfisALT  40270  mgmpropd  40283  isassintop  40354  lidldomn1  40429  lidlmmgm  40433  2zlidl  40442  2zrngamgm  40447  2zrngmmgm  40454  rnghmsscmap  40484  rnghmsubcsetclem2  40486  rngcinv  40491  rngccatidALTV  40499  rngcinvALTV  40503  funcrngcsetc  40508  funcrngcsetcALT  40509  rhmsscmap  40530  rhmsubcsetclem2  40532  rhmsubcrngclem2  40538  ringcinv  40542  funcringcsetc  40545  funcringcsetcALTV2lem9  40554  ringccatidALTV  40562  ringcinvALTV  40566  srhmsubc  40586  rhmsubclem4  40599  srhmsubcALTV  40605  rhmsubcALTVlem4  40618  gsumpr  40650  lmodvsmdi  40675  ply1mulgsumlem1  40686  ply1mulgsumlem2  40687  lincdifsn  40725  lincsumcl  40732  lincscmcl  40733  lincext3  40757  lindslinindsimp1  40758  lindslinindsimp2lem5  40763  snlindsntor  40772  lincresunit2  40779  lincresunit3lem2  40781  lincresunit3  40782  zgtp1leeq  40827  m1modmmod  40832  nn0o  40837  elbigo2  40871  fllog2  40887  digexp  40926  dig1  40927  nn0sumshdiglemA  40938  nn0sumshdiglemB  40939
  Copyright terms: Public domain W3C validator