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

Theorem impcom 419
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 27 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 418 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpan9  455  equtr2  1654  19.41  1815  dvelimf  1937  ax11eq  2132  ax11el  2133  mopick  2205  2euex  2215  gencl  2816  2gencl  2817  rspccva  2883  sbcimdv  3052  sseq0  3486  minel  3510  r19.2z  3543  elelpwi  3635  ssuni  3849  disji2  4010  disjiun  4013  trint0  4130  ssexg  4160  pofun  4330  solin  4337  2optocl  4765  3optocl  4766  elrnmpt1  4928  resieq  4965  funimaexg  5329  fnun  5350  fss  5397  fun  5405  dmfex  5424  tz6.12-1  5544  fvelimab  5578  fvmptss  5609  fmptco  5691  fnressn  5705  fressnfv  5707  fnex  5741  funfvima3  5755  f1fveq  5786  isores3  5832  frxp  6225  fnse  6232  reldmtpos  6242  smores  6369  tz7.48-2  6454  tz7.49  6457  oacl  6534  omcl  6535  oecl  6536  oarec  6560  oewordri  6590  oeworde  6591  oelim2  6593  oeoa  6595  oeoelem  6596  oeoe  6597  nnacl  6609  nnmcl  6610  nnecl  6611  nnmsucr  6623  2ecoptocl  6749  undifixp  6852  xpf1o  7023  limensuc  7038  ac6sfi  7101  frfi  7102  difinf  7127  elfiun  7183  dffi3  7184  xpwdomg  7299  preleq  7318  infdiffi  7358  epfrs  7413  rankxpsuc  7552  tskwe  7583  infxpenlem  7641  fseqenlem1  7651  kmlem2  7777  cff1  7884  cflim2  7889  sornom  7903  infpssrlem4  7932  fin23lem26  7951  fin23lem30  7968  fin23lem34  7972  isf32lem11  7989  fin67  8021  isfin7-2  8022  fin1a2lem10  8035  axcc2lem  8062  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  iunfo  8161  tsk0  8385  gruina  8440  grur1a  8441  mulcanenq  8584  reclem2pr  8672  supsrlem  8733  supsr  8734  ax1rid  8783  mulgt1  9615  lbreu  9704  nnaddcl  9768  nnmulcl  9769  fzind  10110  fnn0ind  10111  uzaddcl  10275  xmulasslem2  10602  supxrunb1  10638  supxrunb2  10639  om2uzlti  11013  fsequb  11037  ser1const  11102  expcllem  11114  expeq0  11132  faclbnd  11303  faclbnd6  11312  hashgadd  11359  hashxp  11386  seqcoll  11401  cjexp  11635  absexp  11789  r19.29uz  11834  caubnd  11842  sqreu  11844  climshft  12050  climub  12135  climserle  12136  sumss  12197  sumss2  12199  o1fsum  12271  binom  12288  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  cvgrat  12339  demoivreALT  12481  znnenlem  12490  ruclem8  12515  dvdsfac  12583  smu01lem  12676  dvdslegcd  12695  gcdneg  12705  gcdmultiple  12729  seq1st  12741  alginv  12745  prmdvdsexp  12793  lubss  14225  lubel  14226  frmdgsum  14484  gaass  14751  gsumwrev  14839  cnfldmulg  16406  cnfldexp  16407  clsss  16791  ntrss  16792  restntr  16912  cmpsublem  17126  cmpsub  17127  2ndcrest  17180  txindislem  17327  t0kq  17509  filufint  17615  fbflim2  17672  flftg  17691  alexsubALTlem4  17744  tmdmulg  17775  xmettri2  17905  mettri  17916  metss  18054  lmmbr  18684  caublcls  18734  lmcau  18738  ovolunlem1a  18855  nulmbl2  18894  voliunlem1  18907  iunmbl  18910  volsup  18913  dvlip  19340  dvfsumle  19368  pf1ind  19438  degltlem1  19458  ply1divex  19522  plyco  19623  dvnply2  19667  plydivex  19677  aannenlem2  19709  aaliou3lem2  19723  ulmcau  19772  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  qabvle  20774  ostthlem2  20777  ostth2lem2  20783  isgrpo  20863  opidon  20989  grpomndo  21013  vcdi  21108  vcdir  21109  vcass  21110  nmosetre  21342  hlim2  21771  shscli  21896  chintcli  21910  dfch2  21986  spansncvi  22231  nmopsetretALT  22443  nmfnsetre  22457  lnopl  22494  lnfnl  22511  pjss2coi  22744  pjorthcoi  22749  pjscji  22750  pjssdif2i  22754  pjclem4a  22778  pj3lem1  22786  strlem5  22835  hstrlem5  22843  cvmdi  22904  mdslmd3i  22912  atcv1  22960  atcvat4i  22977  cdj3lem2a  23016  cdj3lem3a  23019  fmptcof2  23229  rnmpt2ss  23239  xrsmulgzz  23307  ssct  23337  disji2f  23354  disjif2  23358  issgon  23484  cvmliftlem15  23829  relexprel  24031  relexpfld  24034  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  rtrclreclem.min  24044  dfon2lem6  24144  tfisg  24204  poseq  24253  wfrlem11  24266  wfrlem12  24267  frrlem4  24284  frrlem5c  24287  frrlem11  24293  nodenselem5  24339  nocvxminlem  24344  nocvxmin  24345  axeuclidlem  24590  idinside  24707  onsucconi  24876  nopsthph  24995  phthps  24996  prjpacp1  25127  prjpacp2  25128  sssu  25141  mapmapmap  25148  injsurinj  25149  domrancur1c  25202  valcurfn1  25204  ubpar  25261  grpodlcan  25376  trran2  25393  ltrran2  25403  rngmgmbs3  25417  mvecrtol2  25477  muldisc  25481  svli2  25484  svs2  25487  svs3  25488  inttop4  25517  apnei  25520  intopcoaconlem3b  25538  qusp  25542  cmptdst  25568  prdnei  25573  limptlimpr2lem1  25574  islimrs4  25582  bwt2  25592  iintlem1  25610  lvsovso  25626  lvsovso2  25627  sigadd  25649  addcanrg  25667  negveud  25668  negveudr  25669  subaddv  25671  fnmulcv  25684  distsava  25689  hdrmp  25706  isder  25707  homgrf  25802  ismonc  25814  cmpmon  25815  iepiclem  25823  isepic  25824  tartarmap  25888  eltintpar  25899  inttaror  25900  prismorcsetlemb  25913  prismorcset2  25918  clscnc  26010  pgapspf  26052  isconcl5a  26101  isconcl5ab  26102  isconcl6a  26103  segline  26141  nbssntrs  26147  bosser  26167  pdiveql  26168  nn0prpw  26239  upixp  26403  welb  26417  sdclem2  26452  metf1o  26469  sstotbnd3  26500  isbndx  26506  ismtycnv  26526  heiborlem4  26538  bfplem1  26546  mzpexpmpt  26823  diophren  26896  expmordi  27032  rmxypos  27034  jm2.17a  27047  jm2.17b  27048  rmygeid  27051  divalgmodcl  27080  jm2.18  27081  jm2.25  27092  jm2.15nn0  27096  jm2.16nn0  27097  pwslnm  27196  isnumbasgrplem1  27266  dgrnznn  27340  dgraalem  27350  symggen  27411  fnchoice  27700  stoweidlem17  27766  2reurex  27959  2reu1  27964  afvfv0bi  28015  afvres  28034  aovmpt4g  28061  ndmaovass  28066  ndmaovdistr  28067  mpt2xopxnop0  28081  nbusgra  28143  nbcusgra  28159  uvtxnbgra  28165  cusgrauvtx  28168  frgra1v  28176  1to2vfriswmgra  28184  1to3vfriswmgra  28185  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT2  28705  e2ebindALT  28706  bnj228  28763  bnj926  28799  bnj1294  28850  bnj229  28916  bnj607  28948  bnj908  28963  bnj953  28971  bnj1118  29014  bnj1174  29033  bnj1388  29063  a12stdy4  29129  cvrat4  29632
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 177  df-an 360
  Copyright terms: Public domain W3C validator