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

Theorem impcom 432
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 33 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 431 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  mpan9  472  ornldOLD  908  bianir  976  bianirOLD  977  19.41v  1820  equtr2  1853  19.41  2027  nfsb4t  2184  2euex  2341  gencl  3112  2gencl  3113  vtocl4g  3151  rspccva  3182  sseq0  3795  minel  3849  r19.2z  3887  elelpwi  3991  eqoreldif  4039  ssuni  4239  disji2  4408  invdisjrab  4411  disjiun  4412  trint0  4533  ssexg  4568  pofun  4788  solin  4795  2optocl  4929  3optocl  4930  elrnmpt1  5100  resieq  5132  funimaexg  5676  fnun  5698  fss  5752  fun  5761  fvelimab  5935  fvmptss  5972  fvn0ssdmfun  6026  fvcofneq  6043  fmptco  6069  fnressn  6089  fressnfv  6091  fvn0fvelrn  6094  fmptsng  6098  fvtp2g  6128  fvtp3g  6129  tpres  6130  fnex  6145  funfvima3  6155  isores3  6239  dmfex  6763  f1o2ndf1  6913  frxp  6915  fnse  6922  ressuppssdif  6945  funsssuppss  6950  suppss  6954  mpt2xopxnop0  6967  reldmtpos  6987  wfrfun  7052  wfrlem12  7053  smores  7077  tfrlem7  7107  tz7.48-2  7165  tz7.49  7168  oacl  7243  omcl  7244  oecl  7245  oarec  7269  oewordri  7299  oeworde  7300  oelim2  7302  oeoa  7304  oeoelem  7305  oeoe  7306  nnacl  7318  nnmcl  7319  nnecl  7320  nnmsucr  7332  2ecoptocl  7460  undifixp  7564  xpf1o  7738  limensuc  7753  ac6sfi  7819  frfi  7820  difinf  7845  f1dmvrnfibi  7862  f1vrnfibi  7863  suppeqfsuppbi  7901  elfiun  7948  dffi3  7949  xpwdomg  8104  preleq  8126  infdiffi  8166  epfrs  8218  rankxpsuc  8356  tskwe  8387  infxpenlem  8447  fseqenlem1  8457  kmlem2  8583  cff1  8690  cflim2  8695  sornom  8709  infpssrlem4  8738  fin23lem26  8757  fin23lem30  8774  fin23lem34  8778  isf32lem11  8795  fin67  8827  isfin7-2  8828  fin1a2lem10  8841  axcc2lem  8868  axdc2lem  8880  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  iunfo  8966  tsk0  9190  gruina  9245  grur1a  9246  mulcanenq  9387  reclem2pr  9475  supsrlem  9537  supsr  9538  ax1rid  9587  negf1o  10051  mulgt1  10466  fiminre  10557  lbreu  10558  nnaddcl  10633  nnmulcl  10634  nn0n0n1ge2b  10935  nn0indd  11034  fzind  11035  fnn0ind  11036  uzaddcl  11217  uzinfi  11240  nn01to3  11259  xmulasslem2  11570  supxrunb1  11607  supxrunb2  11608  infmremnf  11635  infmrp1  11636  uzsubsubfz  11823  elfz1b  11866  elfz0ubfz0  11896  fz0fzdiffz0  11901  elfzmlbmOLD  11903  elfzmlbp  11904  fzofzim  11964  elfzom1elp1fzo  11982  elfzom1p1elfzo  11994  ssfzo12bi  12007  fzonfzoufzol  12013  elfznelfzob  12016  injresinjlem  12025  injresinj  12026  modaddmodup  12154  om2uzlti  12165  fsequb  12189  ssnn0fi  12198  ser1const  12270  expcllem  12284  expeq0  12303  faclbnd  12476  faclbnd6  12485  hasheqf1oi  12535  hashf1rn  12536  hashgadd  12557  hashunx  12566  hashnn0n0nn  12571  hashgt0elex  12579  hashss  12587  hashxp  12605  hashimarni  12610  seqcoll  12626  hash2prb  12631  hashge2el2difr  12636  hash2prv  12641  hash2sspr  12642  brfi1indlem  12647  fi1uzind  12648  brfi1indALT  12651  lswlgt0cl  12714  swrdnd  12784  swrd0  12786  swrdsbslen  12800  swrdspsleq  12801  2swrd1eqwrdeq  12806  swrdswrdlem  12811  swrdswrd  12812  wrd2ind  12830  swrdccatfn  12834  swrdccatin1  12835  swrdccatin12lem2a  12837  swrdccatin2  12839  swrdccatin12lem2  12841  swrdccatin12lem3  12842  swrdccatin12  12843  swrdccat3  12844  swrdccat  12845  swrdccat3blem  12847  repswswrd  12883  repswrevw  12885  cshwmodn  12893  cshwsublen  12894  cshwidxmod  12901  2cshw  12908  cshweqrep  12916  cshw1  12917  2cshwcshw  12920  cshwcshid  12922  cshwcsh2id  12923  wrdlen2i  13015  2swrd2eqwrdeq  13022  wwlktovfo  13027  relexpsucnnl  13089  rtrclreclem3  13117  rtrclreclem4  13118  relexpindlem  13120  cjexp  13207  absexp  13361  r19.29uz  13407  caubnd  13415  sqreu  13417  climshft  13633  climub  13718  climserle  13719  sumss  13783  sumss2  13785  modfsummods  13846  o1fsum  13866  binom  13881  bcxmas  13886  climcndslem1  13900  climcndslem2  13901  cvgrat  13932  clim2prod  13937  prodfn0  13943  prodfrec  13944  ntrivcvgfvn0  13948  fprodn0  14026  fprodefsum  14142  demoivreALT  14248  znnenlem  14257  ruclem8  14282  dvdsfac  14353  smu01lem  14452  dvdslegcd  14471  gcdneg  14483  gcdmultiple  14511  seq1st  14523  alginv  14527  lcmf  14599  lcmftp  14602  lcmfunsnlem2lem2  14605  lcmfunsnlem  14607  lcmfun  14611  ncoprmgcdne1b  14648  prmdvdsexp  14660  ncoprmlnprm  14670  coprmproddvdslem  14672  coprmproddvds  14673  fvprmselgcd1  14996  prmgaplem6  15019  prmgaplem7  15020  prmgaplem8  15021  cshwshashlem1  15059  inveq  15672  catsubcat  15737  initoeu2lem0  15901  initoeu2lem1  15902  funcestrcsetclem8  16025  funcestrcsetclem9  16026  fthestrcsetc  16028  fullestrcsetc  16029  funcsetcestrclem9  16041  fthsetcestrc  16043  fullsetcestrc  16044  lubss  16360  lubel  16361  mgmb1mgm1  16492  frmdgsum  16639  mgm2nsgrplem3  16647  gaass  16944  gsumwrev  17010  symgextf1lem  17054  symgextf1  17055  fvcosymgeq  17063  gsmsymgreq  17066  symgfixelsi  17069  pmtrprfv3  17088  symggen  17104  pmtrprfval  17121  gsumzres  17536  gsumzunsnd  17581  srgmulgass  17757  srgbinom  17771  lmodvsmmulgdi  18119  0ringnnzr  18486  assamulgscm  18567  gsumply1subr  18820  gsummoncoe1  18891  pf1ind  18936  cnfldmulg  18993  cnfldexp  18994  psgndiflemB  19160  matmulcell  19462  mat1dimscm  19492  dmatmul  19514  dmatscmcl  19520  scmataddcl  19533  scmatsubcl  19534  scmatsgrp1  19539  mavmulsolcl  19568  ma1repveval  19588  1marepvmarrepid  19592  symgmatr01lem  19670  slesolvec  19696  cramerimplem2  19701  decpmatmullem  19787  pm2mpf1  19815  mp2pm2mplem4  19825  monmat2matmon  19840  chpscmat  19858  chpscmatgsumbin  19860  fvmptnn04ifb  19867  chfacfscmul0  19874  chfacfscmulgsum  19876  chfacfpmmul0  19878  chfacfpmmulgsum  19880  cpmadugsumlemF  19892  clsss  20061  ntrss  20062  restntr  20190  cmpsublem  20406  cmpsub  20407  2ndcrest  20461  txindislem  20640  t0kq  20825  filufint  20927  fbflim2  20984  flftg  21003  alexsubALTlem4  21057  cnextfvval  21072  tmdmulg  21099  ustuqtop4  21251  xmettri2  21347  mettri  21359  metss  21515  lmmbr  22220  caublcls  22270  lmcau  22274  ovolunlem1a  22441  nulmbl2  22482  voliunlem1  22495  iunmbl  22498  volsup  22501  dvlip  22937  dvfsumle  22965  degltlem1  23013  ply1divex  23079  plyco  23187  dgrnznn  23193  dvnply2  23232  plydivex  23242  aannenlem2  23277  aaliou3lem2  23291  ulmcau  23342  dchrisumlem1  24319  dchrisumlem2  24320  dchrisumlem3  24321  qabvle  24455  ostthlem2  24458  ostth2lem2  24464  axeuclidlem  24984  usgra2edg  25101  usgraedg4  25106  usgraidx2vlem2  25111  nbusgra  25148  nbgraf1olem5  25165  nb3graprlem1  25171  nb3graprlem2  25172  cusgrarn  25179  nbcusgra  25183  cusgrasize2inds  25197  sizeusglecusglem1  25204  uvtxnbgra  25213  iswlkg  25244  wlkn0  25247  usgrwlknloop  25285  redwlk  25328  wlkdvspthlem  25329  usgra2adedgwlkonALT  25336  usgra2wlkspthlem1  25339  usgra2wlkspthlem2  25340  usgra2wlkspth  25341  fargshiftf1  25357  usgrcyclnl1  25360  usgrcyclnl2  25361  nvnencycllem  25363  constr3trllem2  25371  wwlknimp  25407  wlkiswwlk1  25410  wlkiswwlk2  25417  wlklniswwlkn1  25419  wlklniswwlkn2  25420  vfwlkniswwlkn  25426  wwlknext  25444  wwlknredwwlkn  25446  wwlknredwwlkn0  25447  wwlkextfun  25449  wwlkextinj  25450  wwlkextsur  25451  wwlkextproplem3  25463  clwlkisclwwlklem2a1  25499  clwlkisclwwlklem2fv2  25503  clwlkisclwwlklem2a4  25504  clwlkisclwwlklem2a  25505  clwlkisclwwlklem1  25507  clwwlkel  25513  clwwlkf1  25516  clwwlkfo  25517  clwwlknwwlkncl  25520  clwwlkext2edg  25522  wwlkext2clwwlk  25523  wwlksubclwwlk  25524  clwwisshclwwlem  25526  clwwisshclww  25527  clwwisshclwwn  25528  erclwwlktr  25535  clwwlknscsh  25539  erclwwlkntr  25547  eleclclwwlkn  25553  hashecclwwlkn1  25554  usghashecclwwlk  25555  clwlkfclwwlk  25564  clwlkfoclwwlk  25565  el2wlkonot  25589  el2spthonot  25590  el2wlkonotot0  25592  usg2spthonot0  25609  rusgrasn  25665  rusgranumwlk  25677  clwlknclwlkdifs  25680  frgra1v  25718  1to2vfriswmgra  25726  1to3vfriswmgra  25727  3cyclfrgrarn1  25732  4cycl2vnunb  25737  frgrancvvdeqlem3  25752  frgrawopreglem3  25766  frgrawopreglem4  25767  frgrawopreg  25769  frg2woteqm  25779  2spotdisj  25781  2spotiundisj  25782  usg2spot2nb  25785  extwwlkfablem1  25794  clwwlkextfrlem1  25796  extwwlkfablem2  25798  numclwwlkun  25799  numclwwlkovf2ex  25806  numclwwlkovgelim  25809  numclwlk1lem2foa  25811  numclwlk1lem2f1  25814  numclwlk1lem2fo  25815  numclwwlk1  25818  numclwlk2lem2f  25823  numclwlk2lem2f1o  25825  numclwwlk5  25832  frgrareg  25837  frgraregord013  25838  friendship  25842  isgrpo  25916  opidonOLD  26042  grpomndo  26066  vcdi  26163  vcdir  26164  vcass  26165  nmosetre  26397  hlim2  26837  shscli  26962  chintcli  26976  dfch2  27052  spansncvi  27297  nmopsetretALT  27508  nmfnsetre  27522  lnopl  27559  lnfnl  27576  pjss2coi  27809  pjorthcoi  27814  pjscji  27815  pjssdif2i  27819  pjclem4a  27843  pj3lem1  27851  strlem5  27900  hstrlem5  27908  cvmdi  27969  mdslmd3i  27977  atcv1  28025  atcvat4i  28042  cdj3lem2a  28081  cdj3lem3a  28084  iuninc  28172  disji2f  28183  disjif2  28187  fmptcof2  28255  ssct  28293  nnindd  28384  xrsmulgzz  28441  ofldchr  28579  esumfzf  28892  issgon  28947  voliune  29054  volfiniune  29055  rrvsum  29289  bnj228  29545  bnj1294  29631  bnj229  29697  bnj607  29729  bnj908  29744  bnj953  29752  bnj1118  29795  bnj1174  29814  bnj1388  29844  cvmliftlem15  30023  iprodefisumlem  30377  faclimlem1  30380  dfon2lem6  30435  tfisg  30458  poseq  30492  frrlem4  30518  frrlem5c  30521  frrlem11  30527  nodenselem5  30573  nocvxminlem  30578  nocvxmin  30579  idinside  30850  nn0prpw  30978  onsucconi  31096  exlimim  31702  exellim  31705  icoreclin  31718  wl-aleq  31826  fin2so  31890  poimirlem4  31902  poimirlem26  31924  itg2addnclem  31951  upixp  32014  welb  32021  sdclem2  32029  metf1o  32042  sstotbnd3  32066  isbndx  32072  ismtycnv  32092  heiborlem4  32104  bfplem1  32112  ax12eq  32475  ax12el  32476  cvrat4  32971  mzpexpmpt  35550  diophren  35619  expmordi  35759  rmxypos  35761  jm2.17a  35774  jm2.17b  35775  rmygeid  35778  divalgmodcl  35806  jm2.18  35807  jm2.25  35818  jm2.15nn0  35822  jm2.16nn0  35823  pwslnm  35916  isnumbasgrplem1  35924  dgraalem  35971  dgraalemOLD  35972  relexpiidm  36200  relexpmulnn  36205  relexpmulg  36206  relexp01min  36209  relexp0a  36212  relexpxpmin  36213  dvgrat  36563  radcnvrat  36565  sspwimpcf  37222  sspwimpcfVD  37223  e2ebindALT  37231  2reurex  38359  2reu1  38364  eu2ndop1stv  38380  afvfv0bi  38410  afveu  38411  afvres  38430  aovmpt4g  38459  ndmaovass  38464  ndmaovdistr  38465  nltle2tri  38472  smonoord  38474  fzopredsuc  38476  iccpartres  38488  iccpartiltu  38492  iccpartigtl  38493  iccpartgt  38497  icceuelpartlem  38505  gbegt5  38618  bgoldbwt  38634  nnsum3primesgbe  38643  wtgoldbnnsum4prm  38653  bgoldbnnsum3prm  38655  bgoldbtbndlem2  38657  bgoldbtbndlem3  38658  bgoldbtbndlem4  38659  bgoldbtbnd  38660  pfxsuff1eqwrdeq  38704  pfxccatin12lem2  38721  pfxccatin12  38722  pfxccat3  38723  pfxccat3a  38726  cshword2  38734  propeqop  38748  imarnf1pr  38759  funsndifnop  38764  subsubelfzo0  38795  fzoopth  38796  2ffzoeq  38797  usgredgprv  38945  usgrpredgav  38947  usgr2edg  38954  usgridx2vlem2  38965  usgrres1  38999  fusgrfis  39004  usgra2pthspth  39007  usgra2pth  39010  usgrauvtxvd  39014  usgpredgv  39053  usgpredgvALT  39054  usgedgvadf1lem2  39068  usgedgvadf1ALTlem2  39071  usgresvm1  39097  usgfis  39100  usgresvm1ALT  39101  usgfisALT  39104  mgmpropd  39117  isassintop  39188  lidldomn1  39263  lidlmmgm  39267  2zlidl  39276  2zrngamgm  39281  2zrngmmgm  39288  rnghmsscmap  39318  rnghmsubcsetclem2  39320  rngcinv  39325  rngccatidALTV  39333  rngcinvALTV  39337  funcrngcsetc  39342  funcrngcsetcALT  39343  rhmsscmap  39364  rhmsubcsetclem2  39366  rhmsubcrngclem2  39372  ringcinv  39376  funcringcsetc  39379  funcringcsetcALTV2lem9  39388  ringccatidALTV  39396  ringcinvALTV  39400  srhmsubc  39420  rhmsubclem4  39433  srhmsubcALTV  39439  rhmsubcALTVlem4  39452  gsumpr  39486  lmodvsmdi  39511  ply1mulgsumlem1  39522  ply1mulgsumlem2  39523  lincdifsn  39561  lincsumcl  39568  lincscmcl  39569  lincext3  39593  lindslinindsimp1  39594  lindslinindsimp2lem5  39599  snlindsntor  39608  lincresunit2  39615  lincresunit3lem2  39617  lincresunit3  39618  zgtp1leeq  39663  m1modmmod  39668  nn0o  39673  elbigo2  39707  fllog2  39723  digexp  39762  dig1  39763  nn0sumshdiglemA  39774  nn0sumshdiglemB  39775
  Copyright terms: Public domain W3C validator