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  1679  19.41  1846  dvelimf  1969  ax11eq  2165  ax11el  2166  mopick  2238  2euex  2248  gencl  2850  2gencl  2851  rspccva  2917  sbcimdv  3086  sseq0  3520  minel  3544  r19.2z  3577  elelpwi  3669  ssuni  3886  disji2  4047  disjiun  4050  trint0  4167  ssexg  4197  pofun  4367  solin  4374  2optocl  4802  3optocl  4803  elrnmpt1  4965  resieq  5002  funimaexg  5366  fnun  5387  fss  5435  fun  5443  dmfex  5462  tz6.12-1  5582  fvelimab  5616  fvmptss  5647  fmptco  5729  fnressn  5744  fressnfv  5746  fnex  5782  funfvima3  5796  f1fveq  5828  isores3  5874  frxp  6267  fnse  6274  reldmtpos  6284  smores  6411  tz7.48-2  6496  tz7.49  6499  oacl  6576  omcl  6577  oecl  6578  oarec  6602  oewordri  6632  oeworde  6633  oelim2  6635  oeoa  6637  oeoelem  6638  oeoe  6639  nnacl  6651  nnmcl  6652  nnecl  6653  nnmsucr  6665  2ecoptocl  6792  undifixp  6895  xpf1o  7066  limensuc  7081  ac6sfi  7146  frfi  7147  difinf  7172  elfiun  7228  dffi3  7229  xpwdomg  7344  preleq  7363  infdiffi  7403  epfrs  7458  rankxpsuc  7597  tskwe  7628  infxpenlem  7686  fseqenlem1  7696  kmlem2  7822  cff1  7929  cflim2  7934  sornom  7948  infpssrlem4  7977  fin23lem26  7996  fin23lem30  8013  fin23lem34  8017  isf32lem11  8034  fin67  8066  isfin7-2  8067  fin1a2lem10  8080  axcc2lem  8107  axdc2lem  8119  axdc3lem2  8122  axdc3lem4  8124  axdc4lem  8126  iunfo  8206  tsk0  8430  gruina  8485  grur1a  8486  mulcanenq  8629  reclem2pr  8717  supsrlem  8778  supsr  8779  ax1rid  8828  mulgt1  9660  lbreu  9749  nnaddcl  9813  nnmulcl  9814  fzind  10157  fnn0ind  10158  uzaddcl  10322  xmulasslem2  10649  supxrunb1  10685  supxrunb2  10686  om2uzlti  11060  fsequb  11084  ser1const  11149  expcllem  11161  expeq0  11179  faclbnd  11350  faclbnd6  11359  hashgadd  11406  hashxp  11433  seqcoll  11448  cjexp  11682  absexp  11836  r19.29uz  11881  caubnd  11889  sqreu  11891  climshft  12097  climub  12182  climserle  12183  sumss  12244  sumss2  12246  o1fsum  12318  binom  12335  bcxmas  12341  climcndslem1  12355  climcndslem2  12356  cvgrat  12386  demoivreALT  12528  znnenlem  12537  ruclem8  12562  dvdsfac  12630  smu01lem  12723  dvdslegcd  12742  gcdneg  12752  gcdmultiple  12776  seq1st  12788  alginv  12792  prmdvdsexp  12840  lubss  14274  lubel  14275  frmdgsum  14533  gaass  14800  gsumwrev  14888  cnfldmulg  16462  cnfldexp  16463  clsss  16847  ntrss  16848  restntr  16968  cmpsublem  17182  cmpsub  17183  2ndcrest  17236  txindislem  17383  t0kq  17565  filufint  17667  fbflim2  17724  flftg  17743  alexsubALTlem4  17796  tmdmulg  17827  xmettri2  17957  mettri  17968  metss  18106  lmmbr  18737  caublcls  18787  lmcau  18791  ovolunlem1a  18908  nulmbl2  18947  voliunlem1  18960  iunmbl  18963  volsup  18966  dvlip  19393  dvfsumle  19421  pf1ind  19491  degltlem1  19511  ply1divex  19575  plyco  19676  dvnply2  19720  plydivex  19730  aannenlem2  19762  aaliou3lem2  19776  ulmcau  19825  dchrisumlem1  20691  dchrisumlem2  20692  dchrisumlem3  20693  qabvle  20827  ostthlem2  20830  ostth2lem2  20836  isgrpo  20916  opidon  21042  grpomndo  21066  vcdi  21163  vcdir  21164  vcass  21165  nmosetre  21397  hlim2  21826  shscli  21951  chintcli  21965  dfch2  22041  spansncvi  22286  nmopsetretALT  22498  nmfnsetre  22512  lnopl  22549  lnfnl  22566  pjss2coi  22799  pjorthcoi  22804  pjscji  22805  pjssdif2i  22809  pjclem4a  22833  pj3lem1  22841  strlem5  22890  hstrlem5  22898  cvmdi  22959  mdslmd3i  22967  atcv1  23015  atcvat4i  23032  cdj3lem2a  23071  cdj3lem3a  23074  disji2f  23162  disjif2  23166  fmptcof2  23226  rnmpt2ss  23236  ssct  23251  xrsmulgzz  23342  esumfzf  23635  issgon  23682  voliune  23759  volfiniune  23760  rrvsum  23886  cvmliftlem15  24113  relexprel  24315  relexpfld  24318  relexpadd  24319  relexpindlem  24320  rtrclreclem.trans  24327  rtrclreclem.min  24328  clim2prod  24396  ntrivcvgfvn0  24404  faclimlem1  24481  dfon2lem6  24529  tfisg  24589  poseq  24638  wfrlem11  24651  wfrlem12  24652  frrlem4  24669  frrlem5c  24672  frrlem11  24678  nodenselem5  24724  nocvxminlem  24729  nocvxmin  24730  axeuclidlem  24976  idinside  25093  onsucconi  25262  nn0prpw  25388  upixp  25552  welb  25566  sdclem2  25601  metf1o  25618  sstotbnd3  25648  isbndx  25654  ismtycnv  25674  heiborlem4  25686  bfplem1  25694  mzpexpmpt  25971  diophren  26044  expmordi  26180  rmxypos  26182  jm2.17a  26195  jm2.17b  26196  rmygeid  26199  divalgmodcl  26228  jm2.18  26229  jm2.25  26240  jm2.15nn0  26244  jm2.16nn0  26245  pwslnm  26344  isnumbasgrplem1  26414  dgrnznn  26488  dgraalem  26498  symggen  26559  fnchoice  26848  stoweidlem17  26914  2reurex  27107  2reu1  27112  eu2ndop1stv  27128  afvfv0bi  27165  afveu  27166  afvres  27185  aovmpt4g  27214  ndmaovass  27219  ndmaovdistr  27220  fvtp2g  27238  fvtp3g  27239  mpt2xopxnop0  27255  injresinjlem  27276  injresinj  27277  hasheqf1oi  27290  hashunx  27294  usgra2edg  27353  usgraedg4  27357  nbusgra  27377  nbgraf1olem5  27392  nb3graprlem1  27397  nb3graprlem2  27398  nbcusgra  27408  uvtxnbgra  27416  cusgrauvtx  27419  usgrnloop  27467  constr2trl  27494  redwlk  27502  wlkdvspthlem  27503  fargshiftf1  27520  usgrcyclnl1  27524  usgrcyclnl2  27525  nvnencycllem  27527  constr3trllem2  27535  frgra1v  27590  1to2vfriswmgra  27598  1to3vfriswmgra  27599  3cyclfrgrarn1  27604  4cycl2vnunb  27609  frgranbnb  27612  frgrancvvdeqlem3  27624  sspwimpcf  28207  sspwimpcfVD  28208  sspwimpALT2  28216  e2ebindALT  28217  bnj228  28274  bnj926  28310  bnj1294  28361  bnj229  28427  bnj607  28459  bnj908  28474  bnj953  28482  bnj1118  28525  bnj1174  28544  bnj1388  28574  dvelimfOLD7  28877  a12stdy4  28947  cvrat4  29450
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