MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impcom Structured version   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  1700  19.41  1900  19.41OLD  1901  dvelimfOLD  2065  equvini  2079  nfsb4t  2154  ax11eq  2269  ax11el  2270  mopick  2342  2euex  2352  gencl  2976  2gencl  2977  rspccva  3043  sbcimdv  3214  sseq0  3651  minel  3675  r19.2z  3709  elelpwi  3801  ssuni  4029  disji2  4191  disjiun  4194  trint0  4311  ssexg  4341  pofun  4511  solin  4518  2optocl  4945  3optocl  4946  elrnmpt1  5111  resieq  5148  funimaexg  5522  fnun  5543  fss  5591  fun  5599  dmfex  5618  fvelimab  5774  fvmptss  5805  fmptco  5893  fnressn  5910  fressnfv  5912  fvtp2g  5935  fvtp3g  5936  fnex  5953  funfvima3  5967  isores3  6047  f1o2ndf1  6446  frxp  6448  fnse  6455  mpt2xopxnop0  6458  reldmtpos  6479  smores  6606  tz7.48-2  6691  tz7.49  6694  oacl  6771  omcl  6772  oecl  6773  oarec  6797  oewordri  6827  oeworde  6828  oelim2  6830  oeoa  6832  oeoelem  6833  oeoe  6834  nnacl  6846  nnmcl  6847  nnecl  6848  nnmsucr  6860  2ecoptocl  6987  undifixp  7090  xpf1o  7261  limensuc  7276  ac6sfi  7343  frfi  7344  difinf  7369  elfiun  7427  dffi3  7428  xpwdomg  7545  preleq  7564  infdiffi  7604  epfrs  7659  rankxpsuc  7798  tskwe  7829  infxpenlem  7887  fseqenlem1  7897  kmlem2  8023  cff1  8130  cflim2  8135  sornom  8149  infpssrlem4  8178  fin23lem26  8197  fin23lem30  8214  fin23lem34  8218  isf32lem11  8235  fin67  8267  isfin7-2  8268  fin1a2lem10  8281  axcc2lem  8308  axdc2lem  8320  axdc3lem2  8323  axdc3lem4  8325  axdc4lem  8327  iunfo  8406  tsk0  8630  gruina  8685  grur1a  8686  mulcanenq  8829  reclem2pr  8917  supsrlem  8978  supsr  8979  ax1rid  9028  mulgt1  9861  lbreu  9950  nnaddcl  10014  nnmulcl  10015  nn0n0n1ge2b  10273  fzind  10360  fnn0ind  10361  uzaddcl  10525  xmulasslem2  10853  supxrunb1  10890  supxrunb2  10891  elfznelfzob  11185  injresinjlem  11191  injresinj  11192  om2uzlti  11282  fsequb  11306  ser1const  11371  expcllem  11384  expeq0  11402  faclbnd  11573  faclbnd6  11582  hasheqf1oi  11627  hashf1rn  11628  hashgadd  11643  hashunx  11652  hashnn0n0nn  11656  hashgt0elex  11662  hash2prb  11681  hashxp  11689  seqcoll  11704  brfi1indlem  11706  brfi1uzind  11707  cjexp  11947  absexp  12101  r19.29uz  12146  caubnd  12154  sqreu  12156  climshft  12362  climub  12447  climserle  12448  sumss  12510  sumss2  12512  o1fsum  12584  binom  12601  bcxmas  12607  climcndslem1  12621  climcndslem2  12622  cvgrat  12652  demoivreALT  12794  znnenlem  12803  ruclem8  12828  dvdsfac  12896  smu01lem  12989  dvdslegcd  13008  gcdneg  13018  gcdmultiple  13042  seq1st  13054  alginv  13058  prmdvdsexp  13106  lubss  14540  lubel  14541  frmdgsum  14799  gaass  15066  gsumwrev  15154  cnfldmulg  16725  cnfldexp  16726  clsss  17110  ntrss  17111  restntr  17238  cmpsublem  17454  cmpsub  17455  bwth  17465  2ndcrest  17509  txindislem  17657  t0kq  17842  filufint  17944  fbflim2  18001  flftg  18020  alexsubALTlem4  18073  cnextfvval  18088  tmdmulg  18114  ustuqtop4  18266  xmettri2  18362  mettri  18374  metss  18530  lmmbr  19203  caublcls  19253  lmcau  19257  ovolunlem1a  19384  nulmbl2  19423  voliunlem1  19436  iunmbl  19439  volsup  19442  dvlip  19869  dvfsumle  19897  pf1ind  19967  degltlem1  19987  ply1divex  20051  plyco  20152  dvnply2  20196  plydivex  20206  aannenlem2  20238  aaliou3lem2  20252  ulmcau  20303  dchrisumlem1  21175  dchrisumlem2  21176  dchrisumlem3  21177  qabvle  21311  ostthlem2  21314  ostth2lem2  21320  usgra2edg  21394  usgraedg4  21398  usgraidx2vlem2  21403  nbusgra  21432  nbgraf1olem5  21447  nb3graprlem1  21452  nb3graprlem2  21453  cusgrarn  21460  nbcusgra  21464  cusgrasize2inds  21478  sizeusglecusglem1  21485  uvtxnbgra  21494  usgrnloop  21555  redwlk  21598  wlkdvspthlem  21599  fargshiftf1  21616  usgrcyclnl1  21619  usgrcyclnl2  21620  nvnencycllem  21622  constr3trllem2  21630  isgrpo  21776  opidon  21902  grpomndo  21926  vcdi  22023  vcdir  22024  vcass  22025  nmosetre  22257  hlim2  22686  shscli  22811  chintcli  22825  dfch2  22901  spansncvi  23146  nmopsetretALT  23358  nmfnsetre  23372  lnopl  23409  lnfnl  23426  pjss2coi  23659  pjorthcoi  23664  pjscji  23665  pjssdif2i  23669  pjclem4a  23693  pj3lem1  23701  strlem5  23750  hstrlem5  23758  cvmdi  23819  mdslmd3i  23827  atcv1  23875  atcvat4i  23892  cdj3lem2a  23931  cdj3lem3a  23934  iuninc  24003  disji2f  24011  disjif2  24015  fmptcof2  24068  ssct  24093  xrsmulgzz  24192  ofldchr  24236  esumfzf  24451  issgon  24498  voliune  24577  volfiniune  24578  rrvsum  24704  cvmliftlem15  24977  relexprel  25126  relexpfld  25129  relexpadd  25130  relexpindlem  25131  rtrclreclem.trans  25138  rtrclreclem.min  25139  clim2prod  25208  prodfn0  25214  prodfrec  25215  ntrivcvgfvn0  25219  fprodefsum  25290  fprodn0  25295  fprod2dlem  25296  iprodefisumlem  25309  faclimlem1  25354  dfon2lem6  25407  tfisg  25471  poseq  25520  wfrlem11  25540  wfrlem12  25541  frrlem4  25577  frrlem5c  25580  frrlem11  25586  nodenselem5  25632  nocvxminlem  25637  nocvxmin  25638  axeuclidlem  25893  idinside  26010  onsucconi  26179  wl-aleq  26227  itg2addnclem  26246  nn0prpw  26317  upixp  26422  welb  26429  sdclem2  26437  metf1o  26452  sstotbnd3  26476  isbndx  26482  ismtycnv  26502  heiborlem4  26514  bfplem1  26522  mzpexpmpt  26793  diophren  26865  expmordi  27001  rmxypos  27003  jm2.17a  27016  jm2.17b  27017  rmygeid  27020  divalgmodcl  27049  jm2.18  27050  jm2.25  27061  jm2.15nn0  27065  jm2.16nn0  27066  pwslnm  27164  isnumbasgrplem1  27234  dgrnznn  27308  dgraalem  27318  symggen  27379  2reurex  27926  2reu1  27931  eu2ndop1stv  27947  afvfv0bi  27983  afveu  27984  afvres  28003  aovmpt4g  28032  ndmaovass  28037  ndmaovdistr  28038  imarnf1pr  28070  elfzmlbm  28090  elfzmlbp  28091  elfzelfzelfz  28093  fz0fzdiffz0  28103  ubmelfzo  28109  ubmelm1fzo  28110  subsubelfzo0  28118  hashimarni  28142  ccatsymb  28152  swrd0  28155  swrdvalodm2  28160  swrd0swrd  28163  swrdswrdlem  28164  swrdswrd  28165  swrdccatfn  28170  swrdccatin1  28171  swrdccatin12lem3a  28174  swrdccatin2  28176  swrdccatin12lem3  28178  swrdccatin12lem4  28179  swrdccatin12  28180  swrdccat3  28181  swrdccat  28182  swrdccat3blem  28184  cshwidx  28208  2cshwmod  28223  cshweqdif2  28233  cshweqdif2s  28234  cshweqrep  28237  cshw1  28238  cshwsame0  28241  cshwssizelem1a  28242  cshwssizelem2  28244  usgra2pthspth  28258  usgra2wlkspthlem1  28259  usgra2wlkspthlem2  28260  usgra2wlkspth  28261  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  el2wlkonotot0  28292  usg2wlkonot  28303  usg2wotspth  28304  usg2spthonot0  28309  frgra1v  28325  1to2vfriswmgra  28333  1to3vfriswmgra  28334  3cyclfrgrarn1  28339  4cycl2vnunb  28344  frgrancvvdeqlem3  28358  frgrawopreglem3  28372  frgrawopreglem4  28373  frgrawopreg  28375  frg2woteqm  28385  2spotdisj  28387  2spotiundisj  28388  usg2spot2nb  28391  sspwimpcf  28969  sspwimpcfVD  28970  e2ebindALT  28978  bnj228  29039  bnj926  29075  bnj1294  29126  bnj229  29192  bnj607  29224  bnj908  29239  bnj953  29247  bnj1118  29290  bnj1174  29309  bnj1388  29339  dvelimfOLD7  29664  cvrat4  30177
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