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

Theorem impcom 428
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 29 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 427 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  mpan9  467  ornldOLD  900  bianir  968  19.41v  1795  equtr2  1826  19.41  1999  nfsb4t  2154  mopickOLD  2308  2euex  2317  gencl  3089  2gencl  3090  vtocl4g  3128  rspccva  3159  sseq0  3771  minel  3825  r19.2z  3862  elelpwi  3966  ssuni  4213  disji2  4382  invdisjrab  4385  disjiun  4386  trint0  4506  ssexg  4540  pofun  4760  solin  4767  2optocl  4901  3optocl  4902  elrnmpt1  5072  resieq  5104  funimaexg  5646  fnun  5668  fss  5722  fun  5731  fvelimab  5905  fvmptss  5942  fvn0ssdmfun  6000  fvcofneq  6017  fmptco  6043  fnressn  6063  fressnfv  6065  fvn0fvelrn  6068  fmptsng  6072  fvtp2g  6102  fvtp3g  6103  tpres  6104  fnex  6120  funfvima3  6130  isores3  6214  dmfex  6742  f1o2ndf1  6892  frxp  6894  fnse  6901  ressuppssdif  6924  funsssuppss  6929  suppss  6933  mpt2xopxnop0  6946  reldmtpos  6966  wfrfun  7031  wfrlem12  7032  smores  7056  tfrlem7  7086  tz7.48-2  7144  tz7.49  7147  oacl  7222  omcl  7223  oecl  7224  oarec  7248  oewordri  7278  oeworde  7279  oelim2  7281  oeoa  7283  oeoelem  7284  oeoe  7285  nnacl  7297  nnmcl  7298  nnecl  7299  nnmsucr  7311  2ecoptocl  7439  undifixp  7543  xpf1o  7717  limensuc  7732  ac6sfi  7798  frfi  7799  difinf  7824  suppeqfsuppbi  7877  elfiun  7924  dffi3  7925  xpwdomg  8045  preleq  8067  infdiffi  8107  epfrs  8194  rankxpsuc  8332  tskwe  8363  infxpenlem  8423  fseqenlem1  8437  kmlem2  8563  cff1  8670  cflim2  8675  sornom  8689  infpssrlem4  8718  fin23lem26  8737  fin23lem30  8754  fin23lem34  8758  isf32lem11  8775  fin67  8807  isfin7-2  8808  fin1a2lem10  8821  axcc2lem  8848  axdc2lem  8860  axdc3lem2  8863  axdc3lem4  8865  axdc4lem  8867  iunfo  8946  tsk0  9171  gruina  9226  grur1a  9227  mulcanenq  9368  reclem2pr  9456  supsrlem  9518  supsr  9519  ax1rid  9568  mulgt1  10442  lbreu  10533  nnaddcl  10598  nnmulcl  10599  nn0n0n1ge2b  10901  nn0indd  11000  fzind  11001  fnn0ind  11002  uzaddcl  11183  nn01to3  11220  xmulasslem2  11527  supxrunb1  11564  supxrunb2  11565  uzsubsubfz  11761  elfz1b  11803  elfz0ubfz0  11833  fz0fzdiffz0  11838  elfzmlbmOLD  11840  elfzmlbp  11841  fzofzim  11901  elfzom1elp1fzo  11919  elfzom1p1elfzo  11931  ssfzo12bi  11944  fzonfzoufzol  11950  elfznelfzob  11953  injresinjlem  11962  injresinj  11963  modaddmodup  12091  om2uzlti  12102  fsequb  12126  ssnn0fi  12135  ser1const  12207  expcllem  12221  expeq0  12240  faclbnd  12412  faclbnd6  12421  hasheqf1oi  12471  hashf1rn  12472  hashgadd  12493  hashunx  12502  hashnn0n0nn  12507  hashgt0elex  12515  hashss  12523  hashxp  12541  hashimarni  12546  seqcoll  12561  hash2prb  12566  hash2prv  12574  hash2sspr  12575  brfi1indlem  12580  brfi1uzind  12581  lswlgt0cl  12643  swrdnd  12713  swrd0  12715  swrdsbslen  12729  swrdspsleq  12730  2swrd1eqwrdeq  12735  swrdswrdlem  12740  swrdswrd  12741  wrd2ind  12759  swrdccatfn  12763  swrdccatin1  12764  swrdccatin12lem2a  12766  swrdccatin2  12768  swrdccatin12lem2  12770  swrdccatin12lem3  12771  swrdccatin12  12772  swrdccat3  12773  swrdccat  12774  swrdccat3blem  12776  repswswrd  12812  repswrevw  12814  cshwmodn  12822  cshwsublen  12823  cshwidxmod  12830  2cshw  12837  cshweqrep  12845  cshw1  12846  2cshwcshw  12849  cshwcshid  12851  cshwcsh2id  12852  wrdlen2i  12940  2swrd2eqwrdeq  12947  wwlktovfo  12952  relexpsucnnl  13014  rtrclreclem3  13042  rtrclreclem4  13043  relexpindlem  13045  cjexp  13132  absexp  13286  r19.29uz  13332  caubnd  13340  sqreu  13342  climshft  13548  climub  13633  climserle  13634  sumss  13695  sumss2  13697  modfsummods  13758  o1fsum  13778  binom  13793  bcxmas  13798  climcndslem1  13812  climcndslem2  13813  cvgrat  13844  clim2prod  13849  prodfn0  13855  prodfrec  13856  ntrivcvgfvn0  13860  fprodn0  13935  fprodefsum  14039  demoivreALT  14145  znnenlem  14154  ruclem8  14179  dvdsfac  14250  smu01lem  14344  dvdslegcd  14363  gcdneg  14373  gcdmultiple  14397  seq1st  14409  alginv  14413  prmdvdsexp  14464  cshwshashlem1  14789  inveq  15387  catsubcat  15452  initoeu2lem0  15616  initoeu2lem1  15617  funcestrcsetclem8  15740  funcestrcsetclem9  15741  fthestrcsetc  15743  fullestrcsetc  15744  funcsetcestrclem9  15756  fthsetcestrc  15758  fullsetcestrc  15759  lubss  16075  lubel  16076  mgmb1mgm1  16207  frmdgsum  16354  mgm2nsgrplem3  16362  gaass  16659  gsumwrev  16725  symgextf1lem  16769  symgextf1  16770  fvcosymgeq  16778  gsmsymgreq  16781  symgfixelsi  16784  pmtrprfv3  16803  symggen  16819  pmtrprfval  16836  gsumzres  17238  gsumzunsnd  17303  srgmulgass  17502  srgbinom  17516  lmodvsmmulgdi  17867  0ringnnzr  18237  assamulgscm  18319  gsumply1subr  18595  gsummoncoe1  18666  pf1ind  18711  cnfldmulg  18770  cnfldexp  18771  psgndiflemB  18934  matmulcell  19239  mat1dimscm  19269  dmatmul  19291  dmatscmcl  19297  scmataddcl  19310  scmatsubcl  19311  scmatsgrp1  19316  mavmulsolcl  19345  ma1repveval  19365  1marepvmarrepid  19369  symgmatr01lem  19447  slesolvec  19473  cramerimplem2  19478  decpmatmullem  19564  pm2mpf1  19592  mp2pm2mplem4  19602  monmat2matmon  19617  chpscmat  19635  chpscmatgsumbin  19637  fvmptnn04ifb  19644  chfacfscmul0  19651  chfacfscmulgsum  19653  chfacfpmmul0  19655  chfacfpmmulgsum  19657  cpmadugsumlemF  19669  clsss  19847  ntrss  19848  restntr  19976  cmpsublem  20192  cmpsub  20193  2ndcrest  20247  txindislem  20426  t0kq  20611  filufint  20713  fbflim2  20770  flftg  20789  alexsubALTlem4  20842  cnextfvval  20857  tmdmulg  20883  ustuqtop4  21039  xmettri2  21135  mettri  21147  metss  21303  lmmbr  21989  caublcls  22039  lmcau  22043  ovolunlem1a  22199  nulmbl2  22239  voliunlem1  22252  iunmbl  22255  volsup  22258  dvlip  22686  dvfsumle  22714  degltlem1  22764  ply1divex  22829  plyco  22930  dgrnznn  22936  dvnply2  22975  plydivex  22985  aannenlem2  23017  aaliou3lem2  23031  ulmcau  23082  dchrisumlem1  24055  dchrisumlem2  24056  dchrisumlem3  24057  qabvle  24191  ostthlem2  24194  ostth2lem2  24200  axeuclidlem  24682  usgra2edg  24799  usgraedg4  24804  usgraidx2vlem2  24809  nbusgra  24845  nbgraf1olem5  24862  nb3graprlem1  24868  nb3graprlem2  24869  cusgrarn  24876  nbcusgra  24880  cusgrasize2inds  24894  sizeusglecusglem1  24901  uvtxnbgra  24910  iswlkg  24941  wlkn0  24944  usgrnloop  24982  redwlk  25025  wlkdvspthlem  25026  usgra2adedgwlkonALT  25033  usgra2wlkspthlem1  25036  usgra2wlkspthlem2  25037  usgra2wlkspth  25038  fargshiftf1  25054  usgrcyclnl1  25057  usgrcyclnl2  25058  nvnencycllem  25060  constr3trllem2  25068  wwlknimp  25104  wlkiswwlk1  25107  wlkiswwlk2  25114  wlklniswwlkn1  25116  wlklniswwlkn2  25117  vfwlkniswwlkn  25123  wwlknext  25141  wwlknredwwlkn  25143  wwlknredwwlkn0  25144  wwlkextfun  25146  wwlkextinj  25147  wwlkextsur  25148  wwlkextproplem3  25160  clwlkisclwwlklem2a1  25196  clwlkisclwwlklem2fv2  25200  clwlkisclwwlklem2a4  25201  clwlkisclwwlklem2a  25202  clwlkisclwwlklem1  25204  clwwlkel  25210  clwwlkf1  25213  clwwlkfo  25214  clwwlknwwlkncl  25217  clwwlkext2edg  25219  wwlkext2clwwlk  25220  wwlksubclwwlk  25221  clwwisshclwwlem  25223  clwwisshclww  25224  clwwisshclwwn  25225  erclwwlktr  25232  clwwlknscsh  25236  erclwwlkntr  25244  eleclclwwlkn  25250  hashecclwwlkn1  25251  usghashecclwwlk  25252  clwlkfclwwlk  25261  clwlkfoclwwlk  25262  el2wlkonot  25286  el2spthonot  25287  el2wlkonotot0  25289  usg2spthonot0  25306  rusgrasn  25362  rusgranumwlk  25374  clwlknclwlkdifs  25377  frgra1v  25415  1to2vfriswmgra  25423  1to3vfriswmgra  25424  3cyclfrgrarn1  25429  4cycl2vnunb  25434  frgrancvvdeqlem3  25449  frgrawopreglem3  25463  frgrawopreglem4  25464  frgrawopreg  25466  frg2woteqm  25476  2spotdisj  25478  2spotiundisj  25479  usg2spot2nb  25482  extwwlkfablem1  25491  clwwlkextfrlem1  25493  extwwlkfablem2  25495  numclwwlkun  25496  numclwwlkovf2ex  25503  numclwwlkovgelim  25506  numclwlk1lem2foa  25508  numclwlk1lem2f1  25511  numclwlk1lem2fo  25512  numclwwlk1  25515  numclwlk2lem2f  25520  numclwlk2lem2f1o  25522  numclwwlk5  25529  frgrareg  25534  frgraregord013  25535  friendship  25539  isgrpo  25612  opidonOLD  25738  grpomndo  25762  vcdi  25859  vcdir  25860  vcass  25861  nmosetre  26093  hlim2  26523  shscli  26649  chintcli  26663  dfch2  26739  spansncvi  26984  nmopsetretALT  27195  nmfnsetre  27209  lnopl  27246  lnfnl  27263  pjss2coi  27496  pjorthcoi  27501  pjscji  27502  pjssdif2i  27506  pjclem4a  27530  pj3lem1  27538  strlem5  27587  hstrlem5  27595  cvmdi  27656  mdslmd3i  27664  atcv1  27712  atcvat4i  27729  cdj3lem2a  27768  cdj3lem3a  27771  iuninc  27858  disji2f  27869  disjif2  27873  fmptcof2  27941  ssct  27978  nnindd  28062  xrsmulgzz  28118  ofldchr  28257  esumfzf  28516  issgon  28571  voliune  28678  volfiniune  28679  rrvsum  28899  bnj228  29117  bnj1294  29203  bnj229  29269  bnj607  29301  bnj908  29316  bnj953  29324  bnj1118  29367  bnj1174  29386  bnj1388  29416  cvmliftlem15  29595  iprodefisumlem  29949  faclimlem1  29952  dfon2lem6  30007  tfisg  30030  poseq  30064  frrlem4  30090  frrlem5c  30093  frrlem11  30099  nodenselem5  30145  nocvxminlem  30150  nocvxmin  30151  idinside  30422  nn0prpw  30551  onsucconi  30669  exlimim  31258  exellim  31261  icoreclin  31274  wl-aleq  31355  fin2so  31412  itg2addnclem  31439  upixp  31502  welb  31509  sdclem2  31517  metf1o  31530  sstotbnd3  31554  isbndx  31560  ismtycnv  31580  heiborlem4  31592  bfplem1  31600  ax12eq  31964  ax12el  31965  cvrat4  32460  mzpexpmpt  35039  diophren  35108  expmordi  35244  rmxypos  35246  jm2.17a  35259  jm2.17b  35260  rmygeid  35263  divalgmodcl  35291  jm2.18  35292  jm2.25  35303  jm2.15nn0  35307  jm2.16nn0  35308  pwslnm  35402  isnumbasgrplem1  35414  dgraalem  35458  relexpiidm  35683  relexpmulnn  35688  relexpmulg  35689  relexp01min  35692  relexp0a  35695  relexpxpmin  35696  dvgrat  36041  radcnvrat  36043  sspwimpcf  36751  sspwimpcfVD  36752  e2ebindALT  36760  2reurex  37554  2reu1  37559  eu2ndop1stv  37575  afvfv0bi  37605  afveu  37606  afvres  37625  aovmpt4g  37654  ndmaovass  37659  ndmaovdistr  37660  nltle2tri  37667  smonoord  37669  fzopredsuc  37671  iccpartres  37685  iccpartiltu  37689  iccpartigtl  37690  iccpartgt  37694  icceuelpartlem  37702  gbegt5  37815  bgoldbwt  37831  nnsum3primesgbe  37840  wtgoldbnnsum4prm  37850  bgoldbnnsum3prm  37852  bgoldbtbndlem2  37854  bgoldbtbndlem3  37855  bgoldbtbndlem4  37856  bgoldbtbnd  37857  pfxsuff1eqwrdeq  37894  pfxccatin12lem2  37911  pfxccatin12  37912  pfxccat3  37913  pfxccat3a  37916  cshword2  37924  imarnf1pr  37942  f1dmvrnfibi  37945  f1vrnfibi  37946  subsubelfzo0  37970  fzoopth  37971  2ffzoeq  37972  usgra2pthspth  37980  usgra2pth  37983  usgrauvtxvd  37987  usgpredgv  38028  usgpredgvALT  38029  usgedgvadf1lem2  38043  usgedgvadf1ALTlem2  38046  usgresvm1  38072  usgfis  38075  usgresvm1ALT  38076  usgfisALT  38079  mgmpropd  38092  isassintop  38163  lidldomn1  38238  lidlmmgm  38242  2zlidl  38251  2zrngamgm  38256  2zrngmmgm  38263  rnghmsscmap  38293  rnghmsubcsetclem2  38295  rngcinv  38300  rngccatidALTV  38308  rngcinvALTV  38312  funcrngcsetc  38317  funcrngcsetcALT  38318  rhmsscmap  38339  rhmsubcsetclem2  38341  rhmsubcrngclem2  38347  ringcinv  38351  funcringcsetc  38354  funcringcsetcALTV2lem9  38363  ringccatidALTV  38371  ringcinvALTV  38375  srhmsubc  38395  rhmsubclem4  38408  srhmsubcALTV  38414  rhmsubcALTVlem4  38427  gsumpr  38461  lmodvsmdi  38486  ply1mulgsumlem1  38497  ply1mulgsumlem2  38498  lincdifsn  38536  lincsumcl  38543  lincscmcl  38544  lincext3  38568  lindslinindsimp1  38569  lindslinindsimp2lem5  38574  snlindsntor  38583  lincresunit2  38590  lincresunit3lem2  38592  lincresunit3  38593  zgtp1leeq  38639  m1modmmod  38644  nn0o  38649  elbigo2  38683  fllog2  38699  digexp  38738  dig1  38739  nn0sumshdiglemA  38750  nn0sumshdiglemB  38751
  Copyright terms: Public domain W3C validator