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

Theorem impcom 420
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 419 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan9  456  equtr2  1696  19.41  1896  19.41OLD  1897  equvini  2040  dvelimf  2050  ax11eq  2243  ax11el  2244  mopick  2316  2euex  2326  gencl  2944  2gencl  2945  rspccva  3011  sbcimdv  3182  sseq0  3619  minel  3643  r19.2z  3677  elelpwi  3769  ssuni  3997  disji2  4159  disjiun  4162  trint0  4279  ssexg  4309  pofun  4479  solin  4486  2optocl  4912  3optocl  4913  elrnmpt1  5078  resieq  5115  funimaexg  5489  fnun  5510  fss  5558  fun  5566  dmfex  5585  fvelimab  5741  fvmptss  5772  fmptco  5860  fnressn  5877  fressnfv  5879  fvtp2g  5902  fvtp3g  5903  fnex  5920  funfvima3  5934  isores3  6014  f1o2ndf1  6413  frxp  6415  fnse  6422  mpt2xopxnop0  6425  reldmtpos  6446  smores  6573  tz7.48-2  6658  tz7.49  6661  oacl  6738  omcl  6739  oecl  6740  oarec  6764  oewordri  6794  oeworde  6795  oelim2  6797  oeoa  6799  oeoelem  6800  oeoe  6801  nnacl  6813  nnmcl  6814  nnecl  6815  nnmsucr  6827  2ecoptocl  6954  undifixp  7057  xpf1o  7228  limensuc  7243  ac6sfi  7310  frfi  7311  difinf  7336  elfiun  7393  dffi3  7394  xpwdomg  7509  preleq  7528  infdiffi  7568  epfrs  7623  rankxpsuc  7762  tskwe  7793  infxpenlem  7851  fseqenlem1  7861  kmlem2  7987  cff1  8094  cflim2  8099  sornom  8113  infpssrlem4  8142  fin23lem26  8161  fin23lem30  8178  fin23lem34  8182  isf32lem11  8199  fin67  8231  isfin7-2  8232  fin1a2lem10  8245  axcc2lem  8272  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  iunfo  8370  tsk0  8594  gruina  8649  grur1a  8650  mulcanenq  8793  reclem2pr  8881  supsrlem  8942  supsr  8943  ax1rid  8992  mulgt1  9825  lbreu  9914  nnaddcl  9978  nnmulcl  9979  nn0n0n1ge2b  10237  fzind  10324  fnn0ind  10325  uzaddcl  10489  xmulasslem2  10817  supxrunb1  10854  supxrunb2  10855  elfznelfzob  11148  injresinjlem  11154  injresinj  11155  om2uzlti  11245  fsequb  11269  ser1const  11334  expcllem  11347  expeq0  11365  faclbnd  11536  faclbnd6  11545  hasheqf1oi  11590  hashf1rn  11591  hashgadd  11606  hashunx  11615  hashnn0n0nn  11619  hashgt0elex  11625  hash2prb  11644  hashxp  11652  seqcoll  11667  brfi1indlem  11669  brfi1uzind  11670  cjexp  11910  absexp  12064  r19.29uz  12109  caubnd  12117  sqreu  12119  climshft  12325  climub  12410  climserle  12411  sumss  12473  sumss2  12475  o1fsum  12547  binom  12564  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  cvgrat  12615  demoivreALT  12757  znnenlem  12766  ruclem8  12791  dvdsfac  12859  smu01lem  12952  dvdslegcd  12971  gcdneg  12981  gcdmultiple  13005  seq1st  13017  alginv  13021  prmdvdsexp  13069  lubss  14503  lubel  14504  frmdgsum  14762  gaass  15029  gsumwrev  15117  cnfldmulg  16688  cnfldexp  16689  clsss  17073  ntrss  17074  restntr  17200  cmpsublem  17416  cmpsub  17417  2ndcrest  17470  txindislem  17618  t0kq  17803  filufint  17905  fbflim2  17962  flftg  17981  alexsubALTlem4  18034  cnextfvval  18049  tmdmulg  18075  ustuqtop4  18227  xmettri2  18323  mettri  18335  metss  18491  lmmbr  19164  caublcls  19214  lmcau  19218  ovolunlem1a  19345  nulmbl2  19384  voliunlem1  19397  iunmbl  19400  volsup  19403  dvlip  19830  dvfsumle  19858  pf1ind  19928  degltlem1  19948  ply1divex  20012  plyco  20113  dvnply2  20157  plydivex  20167  aannenlem2  20199  aaliou3lem2  20213  ulmcau  20264  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  qabvle  21272  ostthlem2  21275  ostth2lem2  21281  usgra2edg  21355  usgraedg4  21359  usgraidx2vlem2  21364  nbusgra  21393  nbgraf1olem5  21408  nb3graprlem1  21413  nb3graprlem2  21414  cusgrarn  21421  nbcusgra  21425  cusgrasize2inds  21439  sizeusglecusglem1  21446  uvtxnbgra  21455  usgrnloop  21516  redwlk  21559  wlkdvspthlem  21560  fargshiftf1  21577  usgrcyclnl1  21580  usgrcyclnl2  21581  nvnencycllem  21583  constr3trllem2  21591  isgrpo  21737  opidon  21863  grpomndo  21887  vcdi  21984  vcdir  21985  vcass  21986  nmosetre  22218  hlim2  22647  shscli  22772  chintcli  22786  dfch2  22862  spansncvi  23107  nmopsetretALT  23319  nmfnsetre  23333  lnopl  23370  lnfnl  23387  pjss2coi  23620  pjorthcoi  23625  pjscji  23626  pjssdif2i  23630  pjclem4a  23654  pj3lem1  23662  strlem5  23711  hstrlem5  23719  cvmdi  23780  mdslmd3i  23788  atcv1  23836  atcvat4i  23853  cdj3lem2a  23892  cdj3lem3a  23895  iuninc  23964  disji2f  23972  disjif2  23976  fmptcof2  24029  ssct  24054  xrsmulgzz  24153  ofldchr  24197  esumfzf  24412  issgon  24459  voliune  24538  volfiniune  24539  rrvsum  24665  cvmliftlem15  24938  relexprel  25087  relexpfld  25090  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  rtrclreclem.min  25100  clim2prod  25169  prodfn0  25175  prodfrec  25176  ntrivcvgfvn0  25180  fprodefsum  25251  fprodn0  25256  fprod2dlem  25257  iprodefisumlem  25270  faclimlem1  25310  dfon2lem6  25358  tfisg  25418  poseq  25467  wfrlem11  25480  wfrlem12  25481  frrlem4  25498  frrlem5c  25501  frrlem11  25507  nodenselem5  25553  nocvxminlem  25558  nocvxmin  25559  axeuclidlem  25805  idinside  25922  onsucconi  26091  itg2addnclem  26155  nn0prpw  26216  upixp  26321  welb  26328  sdclem2  26336  metf1o  26351  sstotbnd3  26375  isbndx  26381  ismtycnv  26401  heiborlem4  26413  bfplem1  26421  mzpexpmpt  26692  diophren  26764  expmordi  26900  rmxypos  26902  jm2.17a  26915  jm2.17b  26916  rmygeid  26919  divalgmodcl  26948  jm2.18  26949  jm2.25  26960  jm2.15nn0  26964  jm2.16nn0  26965  pwslnm  27064  isnumbasgrplem1  27134  dgrnznn  27208  dgraalem  27218  symggen  27279  2reurex  27826  2reu1  27831  eu2ndop1stv  27847  afvfv0bi  27883  afveu  27884  afvres  27903  aovmpt4g  27932  ndmaovass  27937  ndmaovdistr  27938  imarnf1pr  27965  elfzmlbm  27977  elfzmlbp  27978  elfzelfzelfz  27981  ubmelfzo  27986  ubmelm1fzo  27987  hashimarni  27995  swrd0  28002  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  usgra2wlkspth  28038  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  usg2wlkonot  28080  usg2wotspth  28081  usg2spthonot0  28086  frgra1v  28102  1to2vfriswmgra  28110  1to3vfriswmgra  28111  3cyclfrgrarn1  28116  4cycl2vnunb  28121  frgrancvvdeqlem3  28135  frgrawopreglem3  28149  frgrawopreglem4  28150  frgrawopreg  28152  frg2woteqm  28162  2spotdisj  28164  2spotiundisj  28165  usg2spot2nb  28168  sspwimpcf  28741  sspwimpcfVD  28742  e2ebindALT  28751  bnj228  28808  bnj926  28844  bnj1294  28895  bnj229  28961  bnj607  28993  bnj908  29008  bnj953  29016  bnj1118  29059  bnj1174  29078  bnj1388  29108  dvelimfOLD7  29411  cvrat4  29925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator