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

Theorem impcom 430
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 429 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  mpan9  469  ornldOLD  899  bianir  967  19.41v  1772  equtr2  1803  19.41  1972  nfsb4t  2131  ax12eq  2272  ax12el  2273  mopickOLD  2357  2euex  2366  gencl  3139  2gencl  3140  vtocl4g  3178  rspccva  3209  sseq0  3826  minel  3885  r19.2z  3921  elelpwi  4026  ssuni  4273  disji2  4443  invdisjrab  4446  disjiun  4447  trint0  4567  ssexg  4602  pofun  4825  solin  4832  2optocl  5086  3optocl  5087  elrnmpt1  5261  resieq  5294  funimaexg  5671  fnun  5693  fss  5745  fun  5754  fvelimab  5929  fvmptss  5965  fvn0ssdmfun  6023  fvcofneq  6040  fmptco  6065  fnressn  6084  fressnfv  6086  fvn0fvelrn  6089  fmptsng  6093  fvtp2g  6123  fvtp3g  6124  tpres  6125  fnex  6140  funfvima3  6150  isores3  6232  dmfex  6757  f1o2ndf1  6907  frxp  6909  fnse  6916  ressuppssdif  6939  funsssuppss  6944  suppss  6948  mpt2xopxnop0  6961  reldmtpos  6981  smores  7041  tfrlem7  7070  tz7.48-2  7125  tz7.49  7128  oacl  7203  omcl  7204  oecl  7205  oarec  7229  oewordri  7259  oeworde  7260  oelim2  7262  oeoa  7264  oeoelem  7265  oeoe  7266  nnacl  7278  nnmcl  7279  nnecl  7280  nnmsucr  7292  2ecoptocl  7420  undifixp  7524  xpf1o  7698  limensuc  7713  ac6sfi  7782  frfi  7783  difinf  7808  suppeqfsuppbi  7861  elfiun  7908  dffi3  7909  xpwdomg  8029  preleq  8051  infdiffi  8091  epfrs  8179  rankxpsuc  8317  tskwe  8348  infxpenlem  8408  fseqenlem1  8422  kmlem2  8548  cff1  8655  cflim2  8660  sornom  8674  infpssrlem4  8703  fin23lem26  8722  fin23lem30  8739  fin23lem34  8743  isf32lem11  8760  fin67  8792  isfin7-2  8793  fin1a2lem10  8806  axcc2lem  8833  axdc2lem  8845  axdc3lem2  8848  axdc3lem4  8850  axdc4lem  8852  iunfo  8931  tsk0  9158  gruina  9213  grur1a  9214  mulcanenq  9355  reclem2pr  9443  supsrlem  9505  supsr  9506  ax1rid  9555  mulgt1  10422  lbreu  10513  nnaddcl  10578  nnmulcl  10579  nn0n0n1ge2b  10881  nn0indd  10982  fzind  10983  fnn0ind  10984  uzaddcl  11162  nn01to3  11200  xmulasslem2  11499  supxrunb1  11536  supxrunb2  11537  uzsubsubfz  11732  elfz1b  11773  elfz0ubfz0  11803  fz0fzdiffz0  11808  elfzmlbmOLD  11810  elfzmlbp  11811  fzofzim  11867  elfzom1elp1fzo  11885  elfzom1p1elfzo  11897  ssfzo12bi  11909  fzonfzoufzol  11915  elfznelfzob  11918  injresinjlem  11927  injresinj  11928  modaddmodup  12052  om2uzlti  12063  fsequb  12087  ssnn0fi  12096  ser1const  12165  expcllem  12179  expeq0  12198  faclbnd  12370  faclbnd6  12379  hasheqf1oi  12426  hashf1rn  12427  hashgadd  12447  hashunx  12456  hashnn0n0nn  12461  hashgt0elex  12469  hashss  12477  hashxp  12495  hashimarni  12500  seqcoll  12515  hash2prb  12520  hash2prv  12528  hash2sspr  12529  brfi1indlem  12534  brfi1uzind  12535  lswlgt0cl  12597  swrdnd  12667  swrd0  12669  swrdsbslen  12684  swrdspsleq  12685  2swrd1eqwrdeq  12690  swrdswrdlem  12695  swrdswrd  12696  wrd2ind  12714  swrdccatfn  12718  swrdccatin1  12719  swrdccatin12lem2a  12721  swrdccatin2  12723  swrdccatin12lem2  12725  swrdccatin12lem3  12726  swrdccatin12  12727  swrdccat3  12728  swrdccat  12729  swrdccat3blem  12731  repswswrd  12767  repswrevw  12769  cshwmodn  12777  cshwsublen  12778  cshwidxmod  12785  2cshw  12792  cshweqrep  12800  cshw1  12801  2cshwcshw  12804  cshwcshid  12806  cshwcsh2id  12807  wrdlen2i  12895  2swrd2eqwrdeq  12902  wwlktovfo  12907  cjexp  12994  absexp  13148  r19.29uz  13194  caubnd  13202  sqreu  13204  climshft  13410  climub  13495  climserle  13496  sumss  13557  sumss2  13559  modfsummods  13618  o1fsum  13638  binom  13653  bcxmas  13658  climcndslem1  13672  climcndslem2  13673  cvgrat  13703  clim2prod  13708  prodfn0  13714  prodfrec  13715  ntrivcvgfvn0  13719  fprodn0  13794  fprodefsum  13841  demoivreALT  13947  znnenlem  13956  ruclem8  13981  dvdsfac  14052  smu01lem  14146  dvdslegcd  14165  gcdneg  14175  gcdmultiple  14199  seq1st  14211  alginv  14215  prmdvdsexp  14266  cshwshashlem1  14591  inveq  15189  catsubcat  15254  initoeu2lem0  15418  initoeu2lem1  15419  funcestrcsetclem8  15542  funcestrcsetclem9  15543  fthestrcsetc  15545  fullestrcsetc  15546  funcsetcestrclem9  15558  fthsetcestrc  15560  fullsetcestrc  15561  lubss  15877  lubel  15878  mgmb1mgm1  16009  frmdgsum  16156  mgm2nsgrplem3  16164  gaass  16461  gsumwrev  16527  symgextf1lem  16571  symgextf1  16572  fvcosymgeq  16580  gsmsymgreq  16583  symgfixelsi  16586  pmtrprfv3  16605  symggen  16621  pmtrprfval  16638  gsumzres  17040  gsumzunsnd  17108  srgmulgass  17308  srgbinom  17322  lmodvsmmulgdi  17673  0ringnnzr  18043  assamulgscm  18125  gsumply1subr  18401  gsummoncoe1  18472  pf1ind  18517  cnfldmulg  18576  cnfldexp  18577  psgndiflemB  18762  matmulcell  19073  mat1dimscm  19103  dmatmul  19125  dmatscmcl  19131  scmataddcl  19144  scmatsubcl  19145  scmatsgrp1  19150  mavmulsolcl  19179  ma1repveval  19199  1marepvmarrepid  19203  symgmatr01lem  19281  slesolvec  19307  cramerimplem2  19312  decpmatmullem  19398  pm2mpf1  19426  mp2pm2mplem4  19436  monmat2matmon  19451  chpscmat  19469  chpscmatgsumbin  19471  fvmptnn04ifb  19478  chfacfscmul0  19485  chfacfscmulgsum  19487  chfacfpmmul0  19489  chfacfpmmulgsum  19491  cpmadugsumlemF  19503  clsss  19681  ntrss  19682  restntr  19809  cmpsublem  20025  cmpsub  20026  2ndcrest  20080  txindislem  20259  t0kq  20444  filufint  20546  fbflim2  20603  flftg  20622  alexsubALTlem4  20675  cnextfvval  20690  tmdmulg  20716  ustuqtop4  20872  xmettri2  20968  mettri  20980  metss  21136  lmmbr  21822  caublcls  21872  lmcau  21876  ovolunlem1a  22032  nulmbl2  22072  voliunlem1  22085  iunmbl  22088  volsup  22091  dvlip  22519  dvfsumle  22547  degltlem1  22597  ply1divex  22662  plyco  22763  dgrnznn  22769  dvnply2  22808  plydivex  22818  aannenlem2  22850  aaliou3lem2  22864  ulmcau  22915  dchrisumlem1  23799  dchrisumlem2  23800  dchrisumlem3  23801  qabvle  23935  ostthlem2  23938  ostth2lem2  23944  axeuclidlem  24391  usgra2edg  24508  usgraedg4  24513  usgraidx2vlem2  24518  nbusgra  24554  nbgraf1olem5  24571  nb3graprlem1  24577  nb3graprlem2  24578  cusgrarn  24585  nbcusgra  24589  cusgrasize2inds  24603  sizeusglecusglem1  24610  uvtxnbgra  24619  iswlkg  24650  wlkn0  24653  usgrnloop  24691  redwlk  24734  wlkdvspthlem  24735  usgra2adedgwlkonALT  24742  usgra2wlkspthlem1  24745  usgra2wlkspthlem2  24746  usgra2wlkspth  24747  fargshiftf1  24763  usgrcyclnl1  24766  usgrcyclnl2  24767  nvnencycllem  24769  constr3trllem2  24777  wwlknimp  24813  wlkiswwlk1  24816  wlkiswwlk2  24823  wlklniswwlkn1  24825  wlklniswwlkn2  24826  vfwlkniswwlkn  24832  wwlknext  24850  wwlknredwwlkn  24852  wwlknredwwlkn0  24853  wwlkextfun  24855  wwlkextinj  24856  wwlkextsur  24857  wwlkextproplem3  24869  clwlkisclwwlklem2a1  24905  clwlkisclwwlklem2fv2  24909  clwlkisclwwlklem2a4  24910  clwlkisclwwlklem2a  24911  clwlkisclwwlklem1  24913  clwwlkel  24919  clwwlkf1  24922  clwwlkfo  24923  clwwlknwwlkncl  24926  clwwlkext2edg  24928  wwlkext2clwwlk  24929  wwlksubclwwlk  24930  clwwisshclwwlem  24932  clwwisshclww  24933  clwwisshclwwn  24934  erclwwlktr  24941  clwwlknscsh  24945  erclwwlkntr  24953  eleclclwwlkn  24959  hashecclwwlkn1  24960  usghashecclwwlk  24961  clwlkfclwwlk  24970  clwlkfoclwwlk  24971  el2wlkonot  24995  el2spthonot  24996  el2wlkonotot0  24998  usg2spthonot0  25015  rusgrasn  25071  rusgranumwlk  25083  clwlknclwlkdifs  25086  frgra1v  25124  1to2vfriswmgra  25132  1to3vfriswmgra  25133  3cyclfrgrarn1  25138  4cycl2vnunb  25143  frgrancvvdeqlem3  25158  frgrawopreglem3  25172  frgrawopreglem4  25173  frgrawopreg  25175  frg2woteqm  25185  2spotdisj  25187  2spotiundisj  25188  usg2spot2nb  25191  extwwlkfablem1  25200  clwwlkextfrlem1  25202  extwwlkfablem2  25204  numclwwlkun  25205  numclwwlkovf2ex  25212  numclwwlkovgelim  25215  numclwlk1lem2foa  25217  numclwlk1lem2f1  25220  numclwlk1lem2fo  25221  numclwwlk1  25224  numclwlk2lem2f  25229  numclwlk2lem2f1o  25231  numclwwlk5  25238  frgrareg  25243  frgraregord013  25244  friendship  25248  isgrpo  25324  opidonOLD  25450  grpomndo  25474  vcdi  25571  vcdir  25572  vcass  25573  nmosetre  25805  hlim2  26235  shscli  26361  chintcli  26375  dfch2  26451  spansncvi  26696  nmopsetretALT  26908  nmfnsetre  26922  lnopl  26959  lnfnl  26976  pjss2coi  27209  pjorthcoi  27214  pjscji  27215  pjssdif2i  27219  pjclem4a  27243  pj3lem1  27251  strlem5  27300  hstrlem5  27308  cvmdi  27369  mdslmd3i  27377  atcv1  27425  atcvat4i  27442  cdj3lem2a  27481  cdj3lem3a  27484  iuninc  27565  disji2f  27575  disjif2  27579  fmptcof2  27645  ssct  27682  xrsmulgzz  27818  ofldchr  27957  esumfzf  28231  issgon  28284  voliune  28362  volfiniune  28363  rrvsum  28568  cvmliftlem15  28918  relexprel  29232  relexpfld  29235  relexpadd  29236  relexpindlem  29237  rtrclreclem.trans  29244  rtrclreclem.min  29245  iprodefisumlem  29298  faclimlem1  29343  dfon2lem6  29394  tfisg  29458  poseq  29507  wfrlem11  29527  wfrlem12  29528  frrlem4  29564  frrlem5c  29567  frrlem11  29573  nodenselem5  29619  nocvxminlem  29624  nocvxmin  29625  idinside  29896  onsucconi  30064  wl-aleq  30150  fin2so  30202  itg2addnclem  30228  nn0prpw  30303  upixp  30382  welb  30389  sdclem2  30397  metf1o  30410  sstotbnd3  30434  isbndx  30440  ismtycnv  30460  heiborlem4  30472  bfplem1  30480  mzpexpmpt  30839  diophren  30909  expmordi  31045  rmxypos  31047  jm2.17a  31060  jm2.17b  31061  rmygeid  31064  divalgmodcl  31091  jm2.18  31092  jm2.25  31103  jm2.15nn0  31107  jm2.16nn0  31108  pwslnm  31202  isnumbasgrplem1  31212  dgraalem  31256  dvgrat  31355  radcnvrat  31357  2reurex  32347  2reu1  32352  eu2ndop1stv  32368  afvfv0bi  32398  afveu  32399  afvres  32418  aovmpt4g  32447  ndmaovass  32452  ndmaovdistr  32453  pfxsuff1eqwrdeq  32483  pfxccatin12lem2  32500  pfxccatin12  32501  pfxccat3  32502  pfxccat3a  32505  cshword2  32513  imarnf1pr  32531  f1dmvrnfibi  32534  f1vrnfibi  32535  subsubelfzo0  32560  fzoopth  32562  2ffzoeq  32563  usgra2pthspth  32571  usgra2pth  32574  usgrauvtxvd  32578  usgpredgv  32619  usgpredgvALT  32620  usgedgvadf1lem2  32634  usgedgvadf1ALTlem2  32637  usgresvm1  32663  usgfis  32666  usgresvm1ALT  32667  usgfisALT  32670  mgmpropd  32683  isassintop  32754  lidldomn1  32829  lidlmmgm  32833  2zlidl  32842  2zrngamgm  32847  2zrngmmgm  32854  rnghmsscmap  32884  rnghmsubcsetclem2  32886  rngcinv  32891  rngccatidOLD  32899  rngcinvOLD  32903  funcrngcsetc  32908  funcrngcsetcALT  32909  rhmsscmap  32930  rhmsubcsetclem2  32932  rhmsubcrngclem2  32938  ringcinv  32942  funcringcsetc  32945  funcringcsetcOLD2lem9  32954  ringccatidOLD  32962  ringcinvOLD  32966  srhmsubc  32986  rhmsubclem4  32999  srhmsubcOLD  33005  rhmsubcOLDlem4  33018  gsumpr  33052  lmodvsmdi  33077  ply1mulgsumlem1  33088  ply1mulgsumlem2  33089  lincdifsn  33127  lincsumcl  33134  lincscmcl  33135  lincext3  33159  lindslinindsimp1  33160  lindslinindsimp2lem5  33165  snlindsntor  33174  lincresunit2  33181  lincresunit3lem2  33183  lincresunit3  33184  sspwimpcf  33821  sspwimpcfVD  33822  e2ebindALT  33830  bnj228  33891  bnj1294  33977  bnj229  34043  bnj607  34075  bnj908  34090  bnj953  34098  bnj1118  34141  bnj1174  34160  bnj1388  34190  cvrat4  35268
  Copyright terms: Public domain W3C validator