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  897  bianir  965  equtr2  1751  19.41  1920  nfsb4t  2103  ax12eq  2264  ax12el  2265  mopickOLD  2362  mopickOLDOLD  2363  2euex  2375  gencl  3148  2gencl  3149  vtocl4g  3187  rspccva  3218  sbcimdvOLD  3406  sseq0  3822  minel  3887  r19.2z  3923  elelpwi  4027  ssuni  4273  disji2  4440  disjiun  4443  trint0  4563  ssexg  4599  pofun  4822  solin  4829  2optocl  5083  3optocl  5084  elrnmpt1  5257  resieq  5290  funimaexg  5671  fnun  5693  fss  5745  fun  5754  fvelimab  5930  fvmptss  5965  fvn0ssdmfun  6023  fvcofneq  6040  fmptco  6065  fnressn  6084  fressnfv  6086  fvn0fvelrn  6089  fmptsng  6093  fvtp2g  6123  fvtp3g  6124  fnex  6138  funfvima3  6148  isores3  6230  dmfex  6753  f1o2ndf1  6903  frxp  6905  fnse  6912  ressuppssdif  6933  funsssuppss  6938  suppss  6942  mpt2xopxnop0  6955  reldmtpos  6975  smores  7035  tfrlem7  7064  tz7.48-2  7119  tz7.49  7122  oacl  7197  omcl  7198  oecl  7199  oarec  7223  oewordri  7253  oeworde  7254  oelim2  7256  oeoa  7258  oeoelem  7259  oeoe  7260  nnacl  7272  nnmcl  7273  nnecl  7274  nnmsucr  7286  2ecoptocl  7414  undifixp  7517  xpf1o  7691  limensuc  7706  ac6sfi  7776  frfi  7777  difinf  7802  suppeqfsuppbi  7855  elfiun  7902  dffi3  7903  xpwdomg  8023  preleq  8046  infdiffi  8086  epfrs  8174  rankxpsuc  8312  tskwe  8343  infxpenlem  8403  fseqenlem1  8417  kmlem2  8543  cff1  8650  cflim2  8655  sornom  8669  infpssrlem4  8698  fin23lem26  8717  fin23lem30  8734  fin23lem34  8738  isf32lem11  8755  fin67  8787  isfin7-2  8788  fin1a2lem10  8801  axcc2lem  8828  axdc2lem  8840  axdc3lem2  8843  axdc3lem4  8845  axdc4lem  8847  iunfo  8926  tsk0  9153  gruina  9208  grur1a  9209  mulcanenq  9350  reclem2pr  9438  supsrlem  9500  supsr  9501  ax1rid  9550  mulgt1  10413  lbreu  10505  nnaddcl  10570  nnmulcl  10571  nn0n0n1ge2b  10872  fzind  10971  fnn0ind  10972  uzaddcl  11149  nn01to3  11187  xmulasslem2  11486  supxrunb1  11523  supxrunb2  11524  uzsubsubfz  11719  elfz1b  11760  elfz0ubfz0  11788  fz0fzdiffz0  11793  elfzmlbm  11794  elfzmlbp  11795  fzofzim  11849  elfzom1elp1fzo  11863  elfzom1p1elfzo  11875  ssfzo12bi  11887  fzonfzoufzol  11893  elfznelfzob  11896  injresinjlem  11905  injresinj  11906  modaddmodup  12030  om2uzlti  12041  fsequb  12065  ssnn0fi  12074  ser1const  12143  expcllem  12157  expeq0  12176  faclbnd  12348  faclbnd6  12357  hasheqf1oi  12404  hashf1rn  12405  hashgadd  12425  hashunx  12434  hashnn0n0nn  12438  hashgt0elex  12446  hashss  12454  hashxp  12472  hashimarni  12477  seqcoll  12492  hash2prb  12497  hash2prv  12505  hash2sspr  12506  brfi1indlem  12511  brfi1uzind  12512  lswlgt0cl  12569  swrd0  12637  swrdvalodm2  12643  swrdspsleq  12652  2swrd1eqwrdeq  12658  disjxwrd  12659  swrdswrdlem  12663  swrdswrd  12664  wrd2ind  12682  swrdccatfn  12686  swrdccatin1  12687  swrdccatin12lem2a  12689  swrdccatin2  12691  swrdccatin12lem2  12693  swrdccatin12lem3  12694  swrdccatin12  12695  swrdccat3  12696  swrdccat  12697  swrdccat3blem  12699  repswswrd  12735  repswrevw  12737  cshwmodn  12745  cshwsublen  12746  cshwidxmod  12753  2cshw  12760  cshweqrep  12768  cshw1  12769  2cshwcshw  12772  cshwcshid  12774  cshwcsh2id  12775  wrdlen2i  12863  2swrd2eqwrdeq  12870  wwlktovfo  12875  cjexp  12962  absexp  13116  r19.29uz  13162  caubnd  13170  sqreu  13172  climshft  13378  climub  13463  climserle  13464  sumss  13525  sumss2  13527  modfsummods  13586  o1fsum  13606  binom  13621  bcxmas  13626  climcndslem1  13640  climcndslem2  13641  cvgrat  13671  demoivreALT  13813  znnenlem  13822  ruclem8  13847  dvdsfac  13916  smu01lem  14010  dvdslegcd  14029  gcdneg  14039  gcdmultiple  14063  seq1st  14075  alginv  14079  prmdvdsexp  14130  cshwshashlem1  14454  lubss  15624  lubel  15625  mgmb1mgm1  15756  frmdgsum  15901  mgm2nsgrplem3  15909  gaass  16206  gsumwrev  16272  symgextf1lem  16316  symgextf1  16317  fvcosymgeq  16325  gsmsymgreq  16328  symgfixelsi  16331  pmtrprfv3  16350  symggen  16366  pmtrprfval  16383  gsumzres  16785  gsumzunsnd  16853  srgmulgass  17052  srgbinom  17066  lmodvsmmulgdi  17416  0ringnnzr  17785  assamulgscm  17867  gsumply1subr  18143  gsummoncoe1  18214  pf1ind  18259  cnfldmulg  18318  cnfldexp  18319  psgndiflemB  18503  matmulcell  18814  mat1dimscm  18844  dmatmul  18866  dmatscmcl  18872  scmataddcl  18885  scmatsubcl  18886  scmatsgrp1  18891  mavmulsolcl  18920  ma1repveval  18940  1marepvmarrepid  18944  symgmatr01lem  19022  slesolvec  19048  cramerimplem2  19053  decpmatmullem  19139  pm2mpf1  19167  mp2pm2mplem4  19177  monmat2matmon  19192  chpscmat  19210  chpscmatgsumbin  19212  fvmptnn04ifb  19219  chfacfscmul0  19226  chfacfscmulgsum  19228  chfacfpmmul0  19230  chfacfpmmulgsum  19232  cpmadugsumlemF  19244  clsss  19421  ntrss  19422  restntr  19549  cmpsublem  19765  cmpsub  19766  bwthOLD  19777  2ndcrest  19821  txindislem  20000  t0kq  20185  filufint  20287  fbflim2  20344  flftg  20363  alexsubALTlem4  20416  cnextfvval  20431  tmdmulg  20457  ustuqtop4  20613  xmettri2  20709  mettri  20721  metss  20877  lmmbr  21563  caublcls  21613  lmcau  21617  ovolunlem1a  21773  nulmbl2  21813  voliunlem1  21826  iunmbl  21829  volsup  21832  dvlip  22260  dvfsumle  22288  degltlem1  22338  ply1divex  22403  plyco  22504  dvnply2  22548  plydivex  22558  aannenlem2  22590  aaliou3lem2  22604  ulmcau  22655  dchrisumlem1  23538  dchrisumlem2  23539  dchrisumlem3  23540  qabvle  23674  ostthlem2  23677  ostth2lem2  23683  axeuclidlem  24097  usgra2edg  24214  usgraedg4  24219  usgraidx2vlem2  24224  nbusgra  24260  nbgraf1olem5  24277  nb3graprlem1  24283  nb3graprlem2  24284  cusgrarn  24291  nbcusgra  24295  cusgrasize2inds  24309  sizeusglecusglem1  24316  uvtxnbgra  24325  iswlkg  24356  wlkn0  24359  usgrnloop  24397  redwlk  24440  wlkdvspthlem  24441  usgra2adedgwlkonALT  24448  usgra2wlkspthlem1  24451  usgra2wlkspthlem2  24452  usgra2wlkspth  24453  fargshiftf1  24469  usgrcyclnl1  24472  usgrcyclnl2  24473  nvnencycllem  24475  constr3trllem2  24483  wwlknimp  24519  wlkiswwlk1  24522  wlkiswwlk2  24529  wlklniswwlkn1  24531  wlklniswwlkn2  24532  vfwlkniswwlkn  24538  wwlknext  24556  wwlknredwwlkn  24558  wwlknredwwlkn0  24559  wwlkextfun  24561  wwlkextinj  24562  wwlkextsur  24563  wwlkextproplem3  24575  clwlkisclwwlklem2a1  24611  clwlkisclwwlklem2fv2  24615  clwlkisclwwlklem2a4  24616  clwlkisclwwlklem2a  24617  clwlkisclwwlklem1  24619  clwwlkel  24625  clwwlkf1  24628  clwwlkfo  24629  clwwlknwwlkncl  24632  clwwlkext2edg  24634  wwlkext2clwwlk  24635  wwlksubclwwlk  24636  clwwisshclwwlem  24638  clwwisshclww  24639  clwwisshclwwn  24640  erclwwlktr  24647  clwwlknscsh  24651  erclwwlkntr  24659  eleclclwwlkn  24665  hashecclwwlkn1  24666  usghashecclwwlk  24667  clwlkfclwwlk  24676  clwlkfoclwwlk  24677  el2wlkonot  24701  el2spthonot  24702  el2wlkonotot0  24704  usg2spthonot0  24721  rusgrasn  24777  rusgranumwlk  24789  clwlknclwlkdifs  24792  frgra1v  24830  1to2vfriswmgra  24838  1to3vfriswmgra  24839  3cyclfrgrarn1  24844  4cycl2vnunb  24849  frgrancvvdeqlem3  24864  frgrawopreglem3  24878  frgrawopreglem4  24879  frgrawopreg  24881  frg2woteqm  24891  2spotdisj  24893  2spotiundisj  24894  usg2spot2nb  24897  extwwlkfablem1  24906  clwwlkextfrlem1  24908  extwwlkfablem2  24910  numclwwlkun  24911  numclwwlkovf2ex  24918  numclwwlkovgelim  24921  numclwlk1lem2foa  24923  numclwlk1lem2f1  24926  numclwlk1lem2fo  24927  numclwwlk1  24930  numclwlk2lem2f  24935  numclwlk2lem2f1o  24937  numclwwlk5  24944  frgrareg  24949  frgraregord013  24950  friendship  24954  isgrpo  25029  opidonOLD  25155  grpomndo  25179  vcdi  25276  vcdir  25277  vcass  25278  nmosetre  25510  hlim2  25940  shscli  26066  chintcli  26080  dfch2  26156  spansncvi  26401  nmopsetretALT  26613  nmfnsetre  26627  lnopl  26664  lnfnl  26681  pjss2coi  26914  pjorthcoi  26919  pjscji  26920  pjssdif2i  26924  pjclem4a  26948  pj3lem1  26956  strlem5  27005  hstrlem5  27013  cvmdi  27074  mdslmd3i  27082  atcv1  27130  atcvat4i  27147  cdj3lem2a  27186  cdj3lem3a  27189  iuninc  27259  disji2f  27269  disjif2  27273  fmptcof2  27333  ssct  27363  nn0indd  27441  xrsmulgzz  27498  ofldchr  27636  esumfzf  27907  issgon  27955  voliune  28033  volfiniune  28034  rrvsum  28225  cvmliftlem15  28575  relexprel  28889  relexpfld  28892  relexpadd  28893  relexpindlem  28894  rtrclreclem.trans  28901  rtrclreclem.min  28902  clim2prod  28956  prodfn0  28962  prodfrec  28963  ntrivcvgfvn0  28967  fprodefsum  29038  fprodn0  29043  iprodefisumlem  29057  faclimlem1  29102  dfon2lem6  29154  tfisg  29218  poseq  29267  wfrlem11  29287  wfrlem12  29288  frrlem4  29324  frrlem5c  29327  frrlem11  29333  nodenselem5  29379  nocvxminlem  29384  nocvxmin  29385  idinside  29668  onsucconi  29836  wl-aleq  29922  fin2so  29974  itg2addnclem  30000  nn0prpw  30075  upixp  30154  welb  30161  sdclem2  30169  metf1o  30182  sstotbnd3  30206  isbndx  30212  ismtycnv  30232  heiborlem4  30244  bfplem1  30252  mzpexpmpt  30611  diophren  30681  expmordi  30817  rmxypos  30819  jm2.17a  30832  jm2.17b  30833  rmygeid  30836  divalgmodcl  30863  jm2.18  30864  jm2.25  30875  jm2.15nn0  30879  jm2.16nn0  30880  pwslnm  30974  isnumbasgrplem1  30984  dgrnznn  31019  dgraalem  31029  2reurex  31982  2reu1  31987  eu2ndop1stv  32003  afvfv0bi  32033  afveu  32034  afvres  32053  aovmpt4g  32082  ndmaovass  32087  ndmaovdistr  32088  imarnf1pr  32105  f1dmvrnfibi  32108  f1vrnfibi  32109  subsubelfzo0  32134  fzoopth  32136  2ffzoeq  32137  usgra2pthspth  32147  usgra2pth  32150  usgrauvtxvd  32154  usgpredgv  32195  usgpredgvALT  32196  usgedgvadf1lem2  32210  usgedgvadf1ALTlem2  32213  usgresvm1  32239  usgfis  32242  usgresvm1ALT  32243  usgfisALT  32246  isassintop  32299  lidldomn1  32327  lidlmmgm  32331  2zlidl  32340  2zrngamgm  32345  2zrngmmgm  32352  ringccatid  32374  ringcinv  32378  srhmsubc  32395  gsumpr  32435  lmodvsmdi  32462  ply1mulgsumlem1  32473  ply1mulgsumlem2  32474  lincdifsn  32512  lincsumcl  32519  lincscmcl  32520  lincext3  32544  lindslinindsimp1  32545  lindslinindsimp2lem5  32550  snlindsntor  32559  lincresunit2  32566  lincresunit3lem2  32568  lincresunit3  32569  sspwimpcf  33206  sspwimpcfVD  33207  e2ebindALT  33215  bnj228  33276  bnj1294  33361  bnj229  33427  bnj607  33459  bnj908  33474  bnj953  33482  bnj1118  33525  bnj1174  33544  bnj1388  33574  cvrat4  34645
  Copyright terms: Public domain W3C validator