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  1695  19.41  1889  19.41OLD  1890  dvelimf  2033  ax11eq  2228  ax11el  2229  mopick  2301  2euex  2311  gencl  2928  2gencl  2929  rspccva  2995  sbcimdv  3166  sseq0  3603  minel  3627  r19.2z  3661  elelpwi  3753  ssuni  3980  disji2  4141  disjiun  4144  trint0  4261  ssexg  4291  pofun  4461  solin  4468  2optocl  4894  3optocl  4895  elrnmpt1  5060  resieq  5097  funimaexg  5471  fnun  5492  fss  5540  fun  5548  dmfex  5567  fvelimab  5722  fvmptss  5753  fmptco  5841  fnressn  5858  fressnfv  5860  fvtp2g  5883  fvtp3g  5884  fnex  5901  funfvima3  5915  isores3  5995  frxp  6393  fnse  6400  mpt2xopxnop0  6403  reldmtpos  6424  smores  6551  tz7.48-2  6636  tz7.49  6639  oacl  6716  omcl  6717  oecl  6718  oarec  6742  oewordri  6772  oeworde  6773  oelim2  6775  oeoa  6777  oeoelem  6778  oeoe  6779  nnacl  6791  nnmcl  6792  nnecl  6793  nnmsucr  6805  2ecoptocl  6932  undifixp  7035  xpf1o  7206  limensuc  7221  ac6sfi  7288  frfi  7289  difinf  7314  elfiun  7371  dffi3  7372  xpwdomg  7487  preleq  7506  infdiffi  7546  epfrs  7601  rankxpsuc  7740  tskwe  7771  infxpenlem  7829  fseqenlem1  7839  kmlem2  7965  cff1  8072  cflim2  8077  sornom  8091  infpssrlem4  8120  fin23lem26  8139  fin23lem30  8156  fin23lem34  8160  isf32lem11  8177  fin67  8209  isfin7-2  8210  fin1a2lem10  8223  axcc2lem  8250  axdc2lem  8262  axdc3lem2  8265  axdc3lem4  8267  axdc4lem  8269  iunfo  8348  tsk0  8572  gruina  8627  grur1a  8628  mulcanenq  8771  reclem2pr  8859  supsrlem  8920  supsr  8921  ax1rid  8970  mulgt1  9802  lbreu  9891  nnaddcl  9955  nnmulcl  9956  nn0n0n1ge2b  10214  fzind  10301  fnn0ind  10302  uzaddcl  10466  xmulasslem2  10794  supxrunb1  10831  supxrunb2  10832  elfznelfzob  11121  injresinjlem  11127  injresinj  11128  om2uzlti  11218  fsequb  11242  ser1const  11307  expcllem  11320  expeq0  11338  faclbnd  11509  faclbnd6  11518  hasheqf1oi  11563  hashf1rn  11564  hashgadd  11579  hashunx  11588  hashnn0n0nn  11592  hashgt0elex  11598  hash2prb  11617  hashxp  11625  seqcoll  11640  brfi1indlem  11642  brfi1uzind  11643  cjexp  11883  absexp  12037  r19.29uz  12082  caubnd  12090  sqreu  12092  climshft  12298  climub  12383  climserle  12384  sumss  12446  sumss2  12448  o1fsum  12520  binom  12537  bcxmas  12543  climcndslem1  12557  climcndslem2  12558  cvgrat  12588  demoivreALT  12730  znnenlem  12739  ruclem8  12764  dvdsfac  12832  smu01lem  12925  dvdslegcd  12944  gcdneg  12954  gcdmultiple  12978  seq1st  12990  alginv  12994  prmdvdsexp  13042  lubss  14476  lubel  14477  frmdgsum  14735  gaass  15002  gsumwrev  15090  cnfldmulg  16657  cnfldexp  16658  clsss  17042  ntrss  17043  restntr  17169  cmpsublem  17385  cmpsub  17386  2ndcrest  17439  txindislem  17587  t0kq  17772  filufint  17874  fbflim2  17931  flftg  17950  alexsubALTlem4  18003  cnextfvval  18018  tmdmulg  18044  ustuqtop4  18196  xmettri2  18280  mettri  18291  metss  18429  lmmbr  19083  caublcls  19133  lmcau  19137  ovolunlem1a  19260  nulmbl2  19299  voliunlem1  19312  iunmbl  19315  volsup  19318  dvlip  19745  dvfsumle  19773  pf1ind  19843  degltlem1  19863  ply1divex  19927  plyco  20028  dvnply2  20072  plydivex  20082  aannenlem2  20114  aaliou3lem2  20128  ulmcau  20179  dchrisumlem1  21051  dchrisumlem2  21052  dchrisumlem3  21053  qabvle  21187  ostthlem2  21190  ostth2lem2  21196  usgra2edg  21269  usgraedg4  21273  usgraidx2vlem2  21278  nbusgra  21307  nbgraf1olem5  21322  nb3graprlem1  21327  nb3graprlem2  21328  cusgrarn  21335  nbcusgra  21339  cusgrasize2inds  21353  sizeusglecusglem1  21360  uvtxnbgra  21369  usgrnloop  21420  constr2trl  21447  redwlk  21455  wlkdvspthlem  21456  fargshiftf1  21473  usgrcyclnl1  21476  usgrcyclnl2  21477  nvnencycllem  21479  constr3trllem2  21487  isgrpo  21633  opidon  21759  grpomndo  21783  vcdi  21880  vcdir  21881  vcass  21882  nmosetre  22114  hlim2  22543  shscli  22668  chintcli  22682  dfch2  22758  spansncvi  23003  nmopsetretALT  23215  nmfnsetre  23229  lnopl  23266  lnfnl  23283  pjss2coi  23516  pjorthcoi  23521  pjscji  23522  pjssdif2i  23526  pjclem4a  23550  pj3lem1  23558  strlem5  23607  hstrlem5  23615  cvmdi  23676  mdslmd3i  23684  atcv1  23732  atcvat4i  23749  cdj3lem2a  23788  cdj3lem3a  23791  iuninc  23856  disji2f  23864  disjif2  23868  fmptcof2  23919  ssct  23943  xrsmulgzz  24034  ofldchr  24071  esumfzf  24256  issgon  24303  voliune  24380  volfiniune  24381  rrvsum  24492  cvmliftlem15  24765  relexprel  24914  relexpfld  24917  relexpadd  24918  relexpindlem  24919  rtrclreclem.trans  24926  rtrclreclem.min  24927  clim2prod  24996  prodfn0  25002  prodfrec  25003  ntrivcvgfvn0  25007  fprodefsum  25078  fprodn0  25083  faclimlem1  25121  dfon2lem6  25169  tfisg  25229  poseq  25278  wfrlem11  25291  wfrlem12  25292  frrlem4  25309  frrlem5c  25312  frrlem11  25318  nodenselem5  25364  nocvxminlem  25369  nocvxmin  25370  axeuclidlem  25616  idinside  25733  onsucconi  25902  nn0prpw  26018  upixp  26123  welb  26130  sdclem2  26138  metf1o  26153  sstotbnd3  26177  isbndx  26183  ismtycnv  26203  heiborlem4  26215  bfplem1  26223  mzpexpmpt  26494  diophren  26566  expmordi  26702  rmxypos  26704  jm2.17a  26717  jm2.17b  26718  rmygeid  26721  divalgmodcl  26750  jm2.18  26751  jm2.25  26762  jm2.15nn0  26766  jm2.16nn0  26767  pwslnm  26866  isnumbasgrplem1  26936  dgrnznn  27010  dgraalem  27020  symggen  27081  2reurex  27628  2reu1  27633  eu2ndop1stv  27649  afvfv0bi  27686  afveu  27687  afvres  27706  aovmpt4g  27735  ndmaovass  27740  ndmaovdistr  27741  frgra1v  27752  1to2vfriswmgra  27760  1to3vfriswmgra  27761  3cyclfrgrarn1  27766  4cycl2vnunb  27771  frgrancvvdeqlem3  27785  frgrawopreglem3  27799  frgrawopreglem4  27800  frgrawopreg  27802  sspwimpcf  28374  sspwimpcfVD  28375  e2ebindALT  28384  bnj228  28441  bnj926  28477  bnj1294  28528  bnj229  28594  bnj607  28626  bnj908  28641  bnj953  28649  bnj1118  28692  bnj1174  28711  bnj1388  28741  dvelimfOLD7  29044  cvrat4  29558
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