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  1673  19.41  1827  dvelimf  1950  ax11eq  2145  ax11el  2146  mopick  2218  2euex  2228  gencl  2829  2gencl  2830  rspccva  2896  sbcimdv  3065  sseq0  3499  minel  3523  r19.2z  3556  elelpwi  3648  ssuni  3865  disji2  4026  disjiun  4029  trint0  4146  ssexg  4176  pofun  4346  solin  4353  2optocl  4781  3optocl  4782  elrnmpt1  4944  resieq  4981  funimaexg  5345  fnun  5366  fss  5413  fun  5421  dmfex  5440  tz6.12-1  5560  fvelimab  5594  fvmptss  5625  fmptco  5707  fnressn  5721  fressnfv  5723  fnex  5757  funfvima3  5771  f1fveq  5802  isores3  5848  frxp  6241  fnse  6248  reldmtpos  6258  smores  6385  tz7.48-2  6470  tz7.49  6473  oacl  6550  omcl  6551  oecl  6552  oarec  6576  oewordri  6606  oeworde  6607  oelim2  6609  oeoa  6611  oeoelem  6612  oeoe  6613  nnacl  6625  nnmcl  6626  nnecl  6627  nnmsucr  6639  2ecoptocl  6765  undifixp  6868  xpf1o  7039  limensuc  7054  ac6sfi  7117  frfi  7118  difinf  7143  elfiun  7199  dffi3  7200  xpwdomg  7315  preleq  7334  infdiffi  7374  epfrs  7429  rankxpsuc  7568  tskwe  7599  infxpenlem  7657  fseqenlem1  7667  kmlem2  7793  cff1  7900  cflim2  7905  sornom  7919  infpssrlem4  7948  fin23lem26  7967  fin23lem30  7984  fin23lem34  7988  isf32lem11  8005  fin67  8037  isfin7-2  8038  fin1a2lem10  8051  axcc2lem  8078  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  iunfo  8177  tsk0  8401  gruina  8456  grur1a  8457  mulcanenq  8600  reclem2pr  8688  supsrlem  8749  supsr  8750  ax1rid  8799  mulgt1  9631  lbreu  9720  nnaddcl  9784  nnmulcl  9785  fzind  10126  fnn0ind  10127  uzaddcl  10291  xmulasslem2  10618  supxrunb1  10654  supxrunb2  10655  om2uzlti  11029  fsequb  11053  ser1const  11118  expcllem  11130  expeq0  11148  faclbnd  11319  faclbnd6  11328  hashgadd  11375  hashxp  11402  seqcoll  11417  cjexp  11651  absexp  11805  r19.29uz  11850  caubnd  11858  sqreu  11860  climshft  12066  climub  12151  climserle  12152  sumss  12213  sumss2  12215  o1fsum  12287  binom  12304  bcxmas  12310  climcndslem1  12324  climcndslem2  12325  cvgrat  12355  demoivreALT  12497  znnenlem  12506  ruclem8  12531  dvdsfac  12599  smu01lem  12692  dvdslegcd  12711  gcdneg  12721  gcdmultiple  12745  seq1st  12757  alginv  12761  prmdvdsexp  12809  lubss  14241  lubel  14242  frmdgsum  14500  gaass  14767  gsumwrev  14855  cnfldmulg  16422  cnfldexp  16423  clsss  16807  ntrss  16808  restntr  16928  cmpsublem  17142  cmpsub  17143  2ndcrest  17196  txindislem  17343  t0kq  17525  filufint  17631  fbflim2  17688  flftg  17707  alexsubALTlem4  17760  tmdmulg  17791  xmettri2  17921  mettri  17932  metss  18070  lmmbr  18700  caublcls  18750  lmcau  18754  ovolunlem1a  18871  nulmbl2  18910  voliunlem1  18923  iunmbl  18926  volsup  18929  dvlip  19356  dvfsumle  19384  pf1ind  19454  degltlem1  19474  ply1divex  19538  plyco  19639  dvnply2  19683  plydivex  19693  aannenlem2  19725  aaliou3lem2  19739  ulmcau  19788  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  qabvle  20790  ostthlem2  20793  ostth2lem2  20799  isgrpo  20879  opidon  21005  grpomndo  21029  vcdi  21124  vcdir  21125  vcass  21126  nmosetre  21358  hlim2  21787  shscli  21912  chintcli  21926  dfch2  22002  spansncvi  22247  nmopsetretALT  22459  nmfnsetre  22473  lnopl  22510  lnfnl  22527  pjss2coi  22760  pjorthcoi  22765  pjscji  22766  pjssdif2i  22770  pjclem4a  22794  pj3lem1  22802  strlem5  22851  hstrlem5  22859  cvmdi  22920  mdslmd3i  22928  atcv1  22976  atcvat4i  22993  cdj3lem2a  23032  cdj3lem3a  23035  fmptcof2  23244  rnmpt2ss  23254  xrsmulgzz  23322  ssct  23352  disji2f  23369  disjif2  23373  issgon  23499  cvmliftlem15  23844  relexprel  24046  relexpfld  24049  relexpadd  24050  relexpindlem  24051  rtrclreclem.trans  24058  rtrclreclem.min  24059  faclim  24126  dfon2lem6  24215  tfisg  24275  poseq  24324  wfrlem11  24337  wfrlem12  24338  frrlem4  24355  frrlem5c  24358  frrlem11  24364  nodenselem5  24410  nocvxminlem  24415  nocvxmin  24416  axeuclidlem  24662  idinside  24779  onsucconi  24948  nopsthph  25098  phthps  25099  prjpacp1  25230  prjpacp2  25231  sssu  25244  mapmapmap  25251  injsurinj  25252  domrancur1c  25305  valcurfn1  25307  ubpar  25364  grpodlcan  25479  trran2  25496  ltrran2  25506  rngmgmbs3  25520  mvecrtol2  25580  muldisc  25584  svli2  25587  svs2  25590  svs3  25591  inttop4  25620  apnei  25623  intopcoaconlem3b  25641  qusp  25645  cmptdst  25671  prdnei  25676  limptlimpr2lem1  25677  islimrs4  25685  bwt2  25695  iintlem1  25713  lvsovso  25729  lvsovso2  25730  sigadd  25752  addcanrg  25770  negveud  25771  negveudr  25772  subaddv  25774  fnmulcv  25787  distsava  25792  hdrmp  25809  isder  25810  homgrf  25905  ismonc  25917  cmpmon  25918  iepiclem  25926  isepic  25927  tartarmap  25991  eltintpar  26002  inttaror  26003  prismorcsetlemb  26016  prismorcset2  26021  clscnc  26113  pgapspf  26155  isconcl5a  26204  isconcl5ab  26205  isconcl6a  26206  segline  26244  nbssntrs  26250  bosser  26270  pdiveql  26271  nn0prpw  26342  upixp  26506  welb  26520  sdclem2  26555  metf1o  26572  sstotbnd3  26603  isbndx  26609  ismtycnv  26629  heiborlem4  26641  bfplem1  26649  mzpexpmpt  26926  diophren  26999  expmordi  27135  rmxypos  27137  jm2.17a  27150  jm2.17b  27151  rmygeid  27154  divalgmodcl  27183  jm2.18  27184  jm2.25  27195  jm2.15nn0  27199  jm2.16nn0  27200  pwslnm  27299  isnumbasgrplem1  27369  dgrnznn  27443  dgraalem  27453  symggen  27514  fnchoice  27803  stoweidlem17  27869  2reurex  28062  2reu1  28067  eu2ndop1stv  28083  afvfv0bi  28120  afveu  28121  afvres  28140  aovmpt4g  28169  ndmaovass  28174  ndmaovdistr  28175  mpt2xopxnop0  28197  injresinjlem  28214  injresinj  28215  nbusgra  28277  nb3graprlem1  28287  nb3graprlem2  28288  nbcusgra  28298  uvtxnbgra  28306  cusgrauvtx  28309  usgrnloop  28351  redwlk  28364  wlkdvspthlem  28365  fargshiftf1  28382  usgrcyclnl1  28386  usgrcyclnl2  28387  nvnencycllem  28389  constr3trllem2  28397  frgra1v  28422  1to2vfriswmgra  28430  1to3vfriswmgra  28431  3cyclfrgrarn1  28435  4cycl2vnunb  28439  sspwimpcf  29012  sspwimpcfVD  29013  sspwimpALT2  29021  e2ebindALT  29022  bnj228  29079  bnj926  29115  bnj1294  29166  bnj229  29232  bnj607  29264  bnj908  29279  bnj953  29287  bnj1118  29330  bnj1174  29349  bnj1388  29379  dvelimfOLD7  29681  a12stdy4  29751  cvrat4  30254
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