MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impcom Structured version   Visualization 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 32 . 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  910  bianir  978  bianirOLD  979  19.29r  1736  19.41v  1830  equtr2  1869  19.41  2051  nfsb4t  2218  2euex  2373  gencl  3077  2gencl  3078  vtocl4g  3118  rspccva  3149  sseq0  3766  minel  3820  r19.2z  3858  elelpwi  3962  eqoreldif  4013  elpreqpr  4161  ssuni  4220  disji2  4389  invdisjrab  4392  disjiun  4393  trint0  4514  ssexg  4549  pofun  4771  solin  4778  2optocl  4912  3optocl  4913  elrnmpt1  5083  resieq  5115  funimaexg  5660  fnun  5682  fss  5737  fun  5746  fvelimab  5921  fvmptss  5958  fvn0ssdmfun  6013  fvcofneq  6030  fmptco  6056  fnressn  6076  fressnfv  6078  fvn0fvelrn  6081  fmptsng  6085  fvtp2g  6115  fvtp3g  6116  tpres  6117  fnex  6132  funfvima3  6142  isores3  6226  dmfex  6751  f1o2ndf1  6904  frxp  6906  fnse  6913  ressuppssdif  6936  funsssuppss  6941  suppss  6945  mpt2xopxnop0  6961  reldmtpos  6981  wfrfun  7046  wfrlem12  7047  smores  7071  tfrlem7  7101  tz7.48-2  7159  tz7.49  7162  oacl  7237  omcl  7238  oecl  7239  oarec  7263  oewordri  7293  oeworde  7294  oelim2  7296  oeoa  7298  oeoelem  7299  oeoe  7300  nnacl  7312  nnmcl  7313  nnecl  7314  nnmsucr  7326  2ecoptocl  7454  undifixp  7558  ssct  7653  xpf1o  7734  limensuc  7749  ac6sfi  7815  frfi  7816  difinf  7841  f1dmvrnfibi  7858  f1vrnfibi  7859  suppeqfsuppbi  7897  elfiun  7944  dffi3  7945  xpwdomg  8100  preleq  8122  infdiffi  8163  epfrs  8215  rankxpsuc  8353  tskwe  8384  infxpenlem  8444  fseqenlem1  8455  kmlem2  8581  cff1  8688  cflim2  8693  sornom  8707  infpssrlem4  8736  fin23lem26  8755  fin23lem30  8772  fin23lem34  8776  isf32lem11  8793  fin67  8825  isfin7-2  8826  fin1a2lem10  8839  axcc2lem  8866  axdc2lem  8878  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  iunfo  8964  tsk0  9188  gruina  9243  grur1a  9244  mulcanenq  9385  reclem2pr  9473  supsrlem  9535  supsr  9536  ax1rid  9585  negf1o  10049  mulgt1  10464  fiminre  10555  lbreu  10556  nnaddcl  10631  nnmulcl  10632  nn0n0n1ge2b  10933  nn0indd  11032  fzind  11033  fnn0ind  11034  uzaddcl  11215  uzinfi  11238  nn01to3  11257  xmulasslem2  11568  supxrunb1  11605  supxrunb2  11606  infmremnf  11633  infmrp1  11634  uzsubsubfz  11821  elfz1b  11864  elfz0ubfz0  11894  fz0fzdiffz0  11899  elfzmlbmOLD  11901  elfzmlbp  11902  fzofzim  11962  elfzom1elp1fzo  11981  elfzom1p1elfzo  11993  ssfzo12bi  12006  fzonfzoufzol  12012  elfznelfzob  12015  injresinjlem  12024  injresinj  12025  modaddmodup  12153  om2uzlti  12164  fsequb  12188  ssnn0fi  12197  ser1const  12269  expcllem  12283  expeq0  12302  faclbnd  12475  faclbnd6  12484  hasheqf1oi  12534  hashf1rn  12535  hashgadd  12556  hashunx  12565  hashnn0n0nn  12570  hashgt0elex  12578  hashss  12586  hashxp  12606  hashimarni  12611  seqcoll  12627  hash2exprb  12632  hashge2el2difr  12638  elss2prb  12643  brfi1indlem  12649  fi1uzind  12650  brfi1indALT  12653  lswlgt0cl  12716  swrdnd  12788  swrd0  12790  swrdsbslen  12804  swrdspsleq  12805  2swrd1eqwrdeq  12810  swrdswrdlem  12815  swrdswrd  12816  wrd2ind  12834  swrdccatfn  12838  swrdccatin1  12839  swrdccatin12lem2a  12841  swrdccatin2  12843  swrdccatin12lem2  12845  swrdccatin12lem3  12846  swrdccatin12  12847  swrdccat3  12848  swrdccat  12849  swrdccat3blem  12851  repswswrd  12887  repswrevw  12889  cshwmodn  12897  cshwsublen  12898  cshwidxmod  12905  2cshw  12912  cshweqrep  12920  cshw1  12921  2cshwcshw  12924  cshwcshid  12926  cshwcsh2id  12927  wrdlen2i  13021  2swrd2eqwrdeq  13028  wwlktovfo  13033  relexpsucnnl  13095  rtrclreclem3  13123  rtrclreclem4  13124  relexpindlem  13126  cjexp  13213  absexp  13367  r19.29uz  13413  caubnd  13421  sqreu  13423  climshft  13640  climub  13725  climserle  13726  sumss  13790  sumss2  13792  modfsummods  13853  o1fsum  13873  binom  13888  bcxmas  13893  climcndslem1  13907  climcndslem2  13908  cvgrat  13939  clim2prod  13944  prodfn0  13950  prodfrec  13951  ntrivcvgfvn0  13955  fprodn0  14033  fprodefsum  14149  demoivreALT  14255  znnenlem  14264  ruclem8  14289  dvdsfac  14360  smu01lem  14459  dvdslegcd  14478  gcdneg  14490  gcdmultiple  14518  seq1st  14530  alginv  14534  lcmf  14606  lcmftp  14609  lcmfunsnlem2lem2  14612  lcmfunsnlem  14614  lcmfun  14618  ncoprmgcdne1b  14655  prmdvdsexp  14667  ncoprmlnprm  14677  coprmproddvdslem  14679  coprmproddvds  14680  fvprmselgcd1  15003  prmgaplem6  15026  prmgaplem7  15027  prmgaplem8  15028  cshwshashlem1  15066  inveq  15679  catsubcat  15744  initoeu2lem0  15908  initoeu2lem1  15909  funcestrcsetclem8  16032  funcestrcsetclem9  16033  fthestrcsetc  16035  fullestrcsetc  16036  funcsetcestrclem9  16048  fthsetcestrc  16050  fullsetcestrc  16051  lubss  16367  lubel  16368  mgmb1mgm1  16499  frmdgsum  16646  mgm2nsgrplem3  16654  gaass  16951  gsumwrev  17017  symgextf1lem  17061  symgextf1  17062  fvcosymgeq  17070  gsmsymgreq  17073  symgfixelsi  17076  pmtrprfv3  17095  symggen  17111  pmtrprfval  17128  gsumzres  17543  gsumzunsnd  17588  srgmulgass  17764  srgbinom  17778  lmodvsmmulgdi  18126  0ringnnzr  18493  assamulgscm  18574  gsumply1subr  18827  gsummoncoe1  18898  pf1ind  18943  cnfldmulg  19000  cnfldexp  19001  psgndiflemB  19168  matmulcell  19470  mat1dimscm  19500  dmatmul  19522  dmatscmcl  19528  scmataddcl  19541  scmatsubcl  19542  scmatsgrp1  19547  mavmulsolcl  19576  ma1repveval  19596  1marepvmarrepid  19600  symgmatr01lem  19678  slesolvec  19704  cramerimplem2  19709  decpmatmullem  19795  pm2mpf1  19823  mp2pm2mplem4  19833  monmat2matmon  19848  chpscmat  19866  chpscmatgsumbin  19868  fvmptnn04ifb  19875  chfacfscmul0  19882  chfacfscmulgsum  19884  chfacfpmmul0  19886  chfacfpmmulgsum  19888  cpmadugsumlemF  19900  clsss  20069  ntrss  20070  restntr  20198  cmpsublem  20414  cmpsub  20415  2ndcrest  20469  txindislem  20648  t0kq  20833  filufint  20935  fbflim2  20992  flftg  21011  alexsubALTlem4  21065  cnextfvval  21080  tmdmulg  21107  ustuqtop4  21259  xmettri2  21355  mettri  21367  metss  21523  lmmbr  22228  caublcls  22278  lmcau  22282  ovolunlem1a  22449  nulmbl2  22490  voliunlem1  22503  iunmbl  22506  volsup  22509  dvlip  22945  dvfsumle  22973  degltlem1  23021  ply1divex  23087  plyco  23195  dgrnznn  23201  dvnply2  23240  plydivex  23250  aannenlem2  23285  aaliou3lem2  23299  ulmcau  23350  dchrisumlem1  24327  dchrisumlem2  24328  dchrisumlem3  24329  qabvle  24463  ostthlem2  24466  ostth2lem2  24472  axeuclidlem  24992  usgra2edg  25109  usgraedg4  25114  usgraidx2vlem2  25119  nbusgra  25156  nbgraf1olem5  25173  nb3graprlem1  25179  nb3graprlem2  25180  cusgrarn  25187  nbcusgra  25191  cusgrasize2inds  25205  sizeusglecusglem1  25212  uvtxnbgra  25221  iswlkg  25252  wlkn0  25255  usgrwlknloop  25293  redwlk  25336  wlkdvspthlem  25337  usgra2adedgwlkonALT  25344  usgra2wlkspthlem1  25347  usgra2wlkspthlem2  25348  usgra2wlkspth  25349  fargshiftf1  25365  usgrcyclnl1  25368  usgrcyclnl2  25369  nvnencycllem  25371  constr3trllem2  25379  wwlknimp  25415  wlkiswwlk1  25418  wlkiswwlk2  25425  wlklniswwlkn1  25427  wlklniswwlkn2  25428  vfwlkniswwlkn  25434  wwlknext  25452  wwlknredwwlkn  25454  wwlknredwwlkn0  25455  wwlkextfun  25457  wwlkextinj  25458  wwlkextsur  25459  wwlkextproplem3  25471  clwlkisclwwlklem2a1  25507  clwlkisclwwlklem2fv2  25511  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem2a  25513  clwlkisclwwlklem1  25515  clwwlkel  25521  clwwlkf1  25524  clwwlkfo  25525  clwwlknwwlkncl  25528  clwwlkext2edg  25530  wwlkext2clwwlk  25531  wwlksubclwwlk  25532  clwwisshclwwlem  25534  clwwisshclww  25535  clwwisshclwwn  25536  erclwwlktr  25543  clwwlknscsh  25547  erclwwlkntr  25555  eleclclwwlkn  25561  hashecclwwlkn1  25562  usghashecclwwlk  25563  clwlkfclwwlk  25572  clwlkfoclwwlk  25573  el2wlkonot  25597  el2spthonot  25598  el2wlkonotot0  25600  usg2spthonot0  25617  rusgrasn  25673  rusgranumwlk  25685  clwlknclwlkdifs  25688  frgra1v  25726  1to2vfriswmgra  25734  1to3vfriswmgra  25735  3cyclfrgrarn1  25740  4cycl2vnunb  25745  frgrancvvdeqlem3  25760  frgrawopreglem3  25774  frgrawopreglem4  25775  frgrawopreg  25777  frg2woteqm  25787  2spotdisj  25789  2spotiundisj  25790  usg2spot2nb  25793  extwwlkfablem1  25802  clwwlkextfrlem1  25804  extwwlkfablem2  25806  numclwwlkun  25807  numclwwlkovf2ex  25814  numclwwlkovgelim  25817  numclwlk1lem2foa  25819  numclwlk1lem2f1  25822  numclwlk1lem2fo  25823  numclwwlk1  25826  numclwlk2lem2f  25831  numclwlk2lem2f1o  25833  numclwwlk5  25840  frgrareg  25845  frgraregord013  25846  friendship  25850  isgrpo  25924  opidonOLD  26050  grpomndo  26074  vcdi  26171  vcdir  26172  vcass  26173  nmosetre  26405  hlim2  26845  shscli  26970  chintcli  26984  dfch2  27060  spansncvi  27305  nmopsetretALT  27516  nmfnsetre  27530  lnopl  27567  lnfnl  27584  pjss2coi  27817  pjorthcoi  27822  pjscji  27823  pjssdif2i  27827  pjclem4a  27851  pj3lem1  27859  strlem5  27908  hstrlem5  27916  cvmdi  27977  mdslmd3i  27985  atcv1  28033  atcvat4i  28050  cdj3lem2a  28089  cdj3lem3a  28092  iuninc  28176  disji2f  28187  disjif2  28191  fmptcof2  28259  nnindd  28383  xrsmulgzz  28440  ofldchr  28577  esumfzf  28890  issgon  28945  voliune  29052  volfiniune  29053  rrvsum  29287  bnj228  29543  bnj1294  29629  bnj229  29695  bnj607  29727  bnj908  29742  bnj953  29750  bnj1118  29793  bnj1174  29812  bnj1388  29842  cvmliftlem15  30021  iprodefisumlem  30376  faclimlem1  30379  dfon2lem6  30434  tfisg  30457  poseq  30491  frrlem4  30517  frrlem5c  30520  frrlem11  30526  nodenselem5  30574  nocvxminlem  30579  nocvxmin  30580  idinside  30851  nn0prpw  30979  onsucconi  31097  exlimim  31744  exellim  31747  icoreclin  31760  wl-aleq  31868  fin2so  31932  poimirlem4  31944  poimirlem26  31966  itg2addnclem  31993  upixp  32056  welb  32063  sdclem2  32071  metf1o  32084  sstotbnd3  32108  isbndx  32114  ismtycnv  32134  heiborlem4  32146  bfplem1  32154  ax12eq  32512  ax12el  32513  cvrat4  33008  mzpexpmpt  35587  diophren  35656  expmordi  35795  rmxypos  35797  jm2.17a  35810  jm2.17b  35811  rmygeid  35814  divalgmodcl  35842  jm2.18  35843  jm2.25  35854  jm2.15nn0  35858  jm2.16nn0  35859  pwslnm  35952  isnumbasgrplem1  35960  dgraalem  36007  dgraalemOLD  36008  relexpiidm  36296  relexpmulnn  36301  relexpmulg  36302  relexp01min  36305  relexp0a  36308  relexpxpmin  36309  dvgrat  36661  radcnvrat  36663  sspwimpcf  37317  sspwimpcfVD  37318  e2ebindALT  37326  2reurex  38602  2reu1  38607  eu2ndop1stv  38623  afvfv0bi  38654  afveu  38655  afvres  38674  aovmpt4g  38703  ndmaovass  38708  ndmaovdistr  38709  nltle2tri  38716  smonoord  38718  fzopredsuc  38720  iccpartres  38732  iccpartiltu  38736  iccpartigtl  38737  iccpartgt  38741  icceuelpartlem  38749  gbegt5  38862  bgoldbwt  38878  nnsum3primesgbe  38887  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  bgoldbtbndlem2  38901  bgoldbtbndlem3  38902  bgoldbtbndlem4  38903  bgoldbtbnd  38904  pfxsuff1eqwrdeq  38948  pfxccatin12lem2  38965  pfxccatin12  38966  pfxccat3  38967  pfxccat3a  38970  cshword2  38978  falseral0  38986  propeqop  38999  ssrelrn  39012  imarnf1pr  39016  funsndifnop  39022  subsubelfzo0  39062  fzoopth  39063  2ffzoeq  39064  incistruhgr  39171  umgredgprv  39195  umgrpredgav  39230  usgredgprvALT  39278  usgr2edg  39291  usgredg2vlem2  39303  subgrfun  39353  umgrres1lem  39377  upgrres1  39380  fusgrfis  39396  uhgrnbgr0nb  39422  nbgr1vtx  39426  nb3grprlem1  39454  uvtxa01vtx0  39469  cusgrsize2inds  39514  upgrewlkle2  39625  wlk1wlk  39650  upgr1wlkwlk  39651  upgrspths1wlklem  39696  upgrspths1wlk  39697  is01wlklem  39705  usgra2pthspth  39718  usgra2pth  39721  usgrauvtxvd  39725  usgpredgv  39764  usgpredgvALT  39765  usgedgvadf1lem2  39779  usgedgvadf1ALTlem2  39782  usgresvm1  39808  usgfis  39811  usgresvm1ALT  39812  usgfisALT  39815  mgmpropd  39828  isassintop  39899  lidldomn1  39974  lidlmmgm  39978  2zlidl  39987  2zrngamgm  39992  2zrngmmgm  39999  rnghmsscmap  40029  rnghmsubcsetclem2  40031  rngcinv  40036  rngccatidALTV  40044  rngcinvALTV  40048  funcrngcsetc  40053  funcrngcsetcALT  40054  rhmsscmap  40075  rhmsubcsetclem2  40077  rhmsubcrngclem2  40083  ringcinv  40087  funcringcsetc  40090  funcringcsetcALTV2lem9  40099  ringccatidALTV  40107  ringcinvALTV  40111  srhmsubc  40131  rhmsubclem4  40144  srhmsubcALTV  40150  rhmsubcALTVlem4  40163  gsumpr  40195  lmodvsmdi  40220  ply1mulgsumlem1  40231  ply1mulgsumlem2  40232  lincdifsn  40270  lincsumcl  40277  lincscmcl  40278  lincext3  40302  lindslinindsimp1  40303  lindslinindsimp2lem5  40308  snlindsntor  40317  lincresunit2  40324  lincresunit3lem2  40326  lincresunit3  40327  zgtp1leeq  40372  m1modmmod  40377  nn0o  40382  elbigo2  40416  fllog2  40432  digexp  40471  dig1  40472  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484
  Copyright terms: Public domain W3C validator