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

Theorem expcom 425
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
exp.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
expcom  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem expcom
StepHypRef Expression
1 exp.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 29 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ancoms  440  syldan  457  sylan  458  4casesdan  917  dedlema  921  dedlemb  922  cbval2  1989  cbval2OLD  1990  cbvex2  1991  dvelimvOLD  2028  2moswap  2355  2eu2  2361  pm2.61ne  2673  r19.21be  2799  uneqdifeq  3708  ssunsn2  3950  ssuni  4029  uniss2  4038  elpwuni  4170  elssabg  4347  elpw2g  4355  oteqex  4441  epelg  4487  wereu  4570  ordtr2  4617  ordsssuc2  4662  difex2  4706  ordpwsuc  4787  ordsucun  4797  limuni3  4824  ordom  4846  relop  5015  riinint  5118  sotri3  5256  unixpid  5396  cnviin  5401  funopg  5477  fun  5599  tz6.12c  5742  fvmptnf  5814  eldmrexrnb  5869  fmptco  5893  fnressn  5910  fressnfv  5912  fvtp2g  5935  fvtp3g  5936  fconst2g  5938  isores3  6047  isoselem  6053  eloprabga  6152  fo1stres  6362  poxp  6450  soxp  6451  brtpos2  6477  sorpsscmpl  6525  onnseq  6598  smores  6606  smofvon2  6610  oacl  6771  omcl  6772  oecl  6773  oawordri  6785  oalimcl  6795  oaass  6796  oarec  6797  omwordri  6807  omeulem1  6817  omeulem2  6818  oeordi  6822  oeworde  6828  oeoelem  6833  nnacl  6846  nnmcl  6847  nnecl  6848  nnacom  6852  nnaass  6857  nnmsucr  6860  nnmordi  6866  omabs  6882  iiner  6968  th3qlem2  7003  elpmg  7024  pmss12g  7032  mapsn  7047  f1domg  7119  ssdomg  7145  domtriord  7245  php  7283  php3  7285  1sdom  7303  fisseneq  7312  isinf  7314  ssnnfi  7320  dif1enOLD  7332  dif1en  7333  findcard3  7342  frfi  7344  unfi  7366  difinf  7369  fnfi  7376  iunfi  7386  elfi2  7411  marypha1lem  7430  marypha1  7431  oiexg  7496  harword  7525  brwdom  7527  unxpwdom  7549  inf3lemd  7574  inf3lem5  7579  cantnfval2  7616  cantnfle  7618  cantnflt  7619  cnfcom  7649  en3lplem1  7662  tcmin  7672  r1sdom  7692  rankxplim3  7797  cardidm  7838  cardmin2  7877  infxpenlem  7887  fseqenlem1  7897  numacn  7922  alephordi  7947  iscard3  7966  alephinit  7968  carduniima  7969  iunfictbso  7987  dfac5  8001  dfac12lem3  8017  pwsdompw  8076  pwcdadom  8088  cflim2  8135  cfslb2n  8140  cofsmo  8141  cfsmolem  8142  cfcoflem  8144  alephsing  8148  infpssALT  8185  fin23lem34  8218  isf32lem2  8226  isf32lem10  8234  isf32lem12  8236  isfin1-2  8257  hsmexlem4  8301  axcc2lem  8308  domtriomlem  8314  axdc2lem  8320  axdc3lem2  8323  axdc3lem4  8325  axdc4lem  8327  axcclem  8329  ac6num  8351  ac6s  8356  zorn2lem7  8374  ttukeylem5  8385  imadomg  8404  iundom2g  8407  ondomon  8430  ficard  8432  konigthlem  8435  alephreg  8449  pwcfsdom  8450  cfpwsdom  8451  axregndlem1  8469  axregnd  8471  pwfseqlem3  8527  pwxpndom2  8532  pwxpndom  8533  pwcdandom  8534  inawinalem  8556  gchina  8566  wuncval2  8614  tsk0  8630  tskxpss  8639  inatsk  8645  tskuni  8650  gruina  8685  grothac  8697  addclpi  8761  addnidpi  8770  nqereu  8798  mulcanenq  8829  genpnnp  8874  nqpr  8883  prlem934  8902  reclem2pr  8917  suplem1pr  8921  mulcmpblnr  8941  supsrlem  8978  axpre-sup  9036  1re  9082  00id  9233  receu  9659  sup3  9957  peano5nni  9995  nnaddcl  10014  zrevaddcl  10313  zdiv  10332  nneo  10345  zeo2  10348  fzind  10360  fnn0ind  10361  uzwo  10531  uzwoOLD  10532  lbzbi  10556  qrevaddcl  10588  irradd  10590  irrmul  10591  ltsubrp  10635  ltaddrp  10636  icoshft  11011  fzen  11064  elfzm11  11108  uzsplit  11110  injresinjlem  11191  injresinj  11192  om2uzlti  11282  seqcl2  11333  seqfveq2  11337  seqshft2  11341  monoord  11345  seqsplit  11348  seqcaopr3  11350  seqf1olem2a  11353  seqf1o  11356  seqid2  11361  seqhomo  11362  ser1const  11371  expadd  11414  expmul  11417  leexp1a  11430  faccl  11568  facdiv  11570  faclbnd  11573  faclbnd4lem4  11579  faclbnd6  11582  hasheqf1oi  11627  hashf1rn  11628  hashgadd  11643  hashdomi  11646  hashinfxadd  11651  hashunx  11652  hashunsng  11657  elprchashprn2  11659  hashle00  11661  hash1snb  11673  hashmap  11690  hashf1lem2  11697  hashf1  11698  seqcoll  11704  brfi1uzind  11707  sswrd  11729  shftlem  11875  caubnd  12154  rlimcld2  12364  o1dif  12415  climub  12447  climserle  12448  iseraltlem2  12468  sumss  12510  fsum2d  12547  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  bcxmas  12607  climcndslem1  12621  climcndslem2  12622  cvgrat  12652  sin01gt0  12783  ruclem8  12828  ruclem9  12829  dvds2ln  12872  dvdslelem  12886  alzdvds  12891  ndvdsadd  12920  bitsinv1  12946  sadcadd  12962  sadadd2  12964  saddisjlem  12968  smuval2  12986  smupvallem  12987  smu01lem  12989  smupval  12992  smueqlem  12994  smumullem  12996  gcddiv  13041  gcdmultiple  13042  rplpwr  13048  nn0seqcvgd  13053  seq1st  13054  alginv  13058  algcvga  13062  algfx  13063  isprm2  13079  isprm3  13080  prmind2  13082  maxprmfct  13105  prmdvdsexp  13106  pcmpt  13253  prmreclem4  13279  vdwmc2  13339  vdwlem10  13350  ramub2  13374  ramcl  13389  imasleval  13758  divsfval  13764  mreexexlem4d  13864  isssc  14012  istos  14456  frmdgsum  14799  mhmmulg  14914  resghm2b  15016  elsymgbas  15089  gsumwrev  15154  odlem1  15165  odcl2  15193  gexlem1  15205  sylow1lem1  15224  efgi2  15349  efginvrel2  15351  efgsrel  15358  cyggexb  15500  gsummulglem  15528  gsum2d  15538  dmdprd  15551  dprdw  15560  ablfac1eulem  15622  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  cnfldmulg  16725  cnfldexp  16726  obslbs  16949  fctop  17060  mretopd  17148  restopnb  17231  restdis  17234  tgcnp  17309  cncls2  17329  cncls  17330  cnntr  17331  cnsscnp  17335  cmpsub  17455  2ndcsep  17514  1stcelcls  17516  txcn  17650  txlm  17672  xkohaus  17677  qtopres  17722  haushmphlem  17811  cmphmph  17812  conhmph  17813  reghmph  17817  nrmhmph  17818  ptcmpfi  17837  reghaus  17849  fbssfi  17861  fbun  17864  fbfinnfr  17865  isfildlem  17881  fgcl  17902  cfinfil  17917  supfil  17919  ufinffr  17953  fin1aufil  17956  cnpflf  18025  alexsubALTlem3  18072  alexsubALT  18074  cnextfvval  18088  cnextcn  18090  tmdmulg  18114  tmdgsum  18117  tgphaus  18138  tgpt1  18139  mettri  18374  imasdsf1olem  18395  blssexps  18448  blssex  18449  mopni3  18516  metss  18530  metutopOLD  18604  psmetutop  18605  dscmet  18612  rectbntr0  18855  metnrmlem1a  18880  fsumcn  18892  lmmbr  19203  caubl  19252  caublcls  19253  bcthlem5  19273  bcth3  19276  ovolunlem1a  19384  ovoliunnul  19395  ovolicc2lem3  19407  finiunmbl  19430  voliunlem1  19436  volsuplem  19441  volsup  19442  dyadmax  19482  itgfsum  19710  dvnadd  19807  dvnres  19809  cpnord  19813  dvnfre  19830  dvmptfsum  19851  dvlip  19869  pf1ind  19967  fta1g  20082  plyco  20152  dgrcolem1  20183  dgrco  20185  dvnply2  20196  plydivex  20206  plyexmo  20222  aannenlem1  20237  aaliou3lem2  20252  dvntaylp  20279  taylthlem1  20281  ulmval  20288  cxpmul2  20572  scvxcvx  20816  jensenlem2  20818  jensen  20819  ppiub  20980  bcmono  21053  bpos1lem  21058  bposlem5  21064  lgsquad2lem2  21135  dchrisumlem1  21175  dchrisum0flb  21196  pntpbnd1  21272  pntlemf  21291  qabvle  21311  qabvexp  21312  ostthlem2  21314  ostth2lem2  21320  usgraedgprv  21388  usgranloopv  21390  usgraidx2vlem2  21403  usgrafisbase  21420  edgusgranbfin  21451  nb3graprlem2  21453  cusgra2v  21463  cusgrafi  21483  sizeusglecusglem1  21485  sizeusglecusg  21487  usgramaxsize  21488  2trllemH  21544  2trllemE  21545  usgrnloop  21555  spthonepeq  21579  wlkdvspthlem  21599  wlkdvspth  21600  cyclnspth  21610  fargshiftf  21615  fargshiftf1  21616  3v3e3cycl2  21643  3v3e3cycl  21644  4cycl4dv  21646  iseupa  21679  eupatrl  21682  eupath2  21694  elghomlem2  21942  isrngo  21958  rngodm1dm2  21998  rngoridfz  22015  hlim2  22686  elnlfn  23423  stle0i  23734  hstrbi  23761  spansncv2  23788  h1da  23844  fmptcof2  24068  xreceu  24160  tpr2rico  24302  hasheuni  24467  ismeas  24545  rrvsum  24704  dstfrvunirn  24724  subfacp1lem6  24863  cvmliftlem7  24970  cvmliftlem10  24973  cvmlift2lem12  24993  cvmlift3lem4  25001  ghomf1olem  25097  climuzcnv  25100  relexpsucr  25122  relexpsucl  25124  relexpcnv  25125  relexprel  25126  relexpdm  25127  relexprn  25128  relexpfld  25129  relexpadd  25130  relexpindlem  25131  rtrclreclem.trans  25138  rtrclreclem.min  25139  rtrclind  25141  dedekindle  25180  clim2prod  25208  prodfn0  25214  prodfrec  25215  ntrivcvg  25217  prodmo  25254  fprodss  25266  fprodabs  25289  fprodefsum  25290  fprodn0  25295  fprod2d  25297  iprodefisumlem  25309  fprb  25389  dfon2lem9  25410  trpredtr  25500  trpredmintr  25501  dftrpred3g  25503  trpredrec  25508  soseq  25521  wfrlem12  25541  frrlem11  25586  sltval2  25603  sltsolem1  25615  axeuclidlem  25893  axcontlem12  25906  linethru  26079  elhf2  26108  hfext  26116  nndivsub  26199  wl-exeq  26226  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  finminlem  26302  fnessref  26354  lfinpfin  26364  locfincmp  26365  comppfsc  26368  neibastop2lem  26370  fnemeet2  26377  cover2  26396  upixp  26412  sdclem2  26427  fdc  26430  seqpo  26432  metf1o  26442  mettrifi  26444  sstotbnd3  26466  heibor1lem  26499  heiborlem5  26505  heibor  26511  bfplem1  26512  grpokerinj  26541  ispridl2  26629  mzpsubst  26786  jm2.18  27040  wepwsolem  27097  stoweidlem2  27708  stoweidlem17  27723  stoweidlem21  27727  2reu2  27922  afveu  27974  funbrafv  27979  ndmaovass  28027  2elfz2melfz  28091  modifeq2int  28129  euhash1  28135  swrd0  28145  swrdvalodm2  28150  swrdvalodm  28151  swrd0swrd  28153  swrdswrdlem  28154  swrdswrd  28155  swrdccatin1  28161  swrdccatin2  28166  swrdccatin12lem3  28168  swrdccat3  28171  cshwcl  28196  cshwidx  28198  2cshw1lem1  28204  2cshw1lem2  28205  2cshw2lem2  28209  2cshw2lem3  28210  2cshwmod  28213  cshweqdif2s  28224  cshweqrep  28227  cshwssizelem4  28237  usgra2wlkspthlem1  28249  usgra2wlkspthlem2  28250  2wlkonot3v  28285  2spthonot3v  28286  usg2wlkonot  28293  usg2wotspth  28294  usgfidegfi  28303  frgra2v  28316  frgra3vlem1  28317  3vfriswmgra  28322  1to2vfriswmgra  28323  1to3vfriswmgra  28324  2pthfrgra  28328  3cyclfrgrarn1  28329  3cyclfrgrarn  28330  3cyclfrgrarn2  28331  4cycl2vnunb  28334  vdn0frgrav2  28341  vdgn0frgrav2  28342  frgrancvvdeqlem4  28349  frgrancvvdeqlemB  28354  frgrancvvdeqlemC  28355  frgrawopreglem2  28361  frgrawopreglem4  28363  frgrawopreg  28365  frgraregorufr0  28368  frgraeu  28370  frg2woteqm  28375  2spotmdisj  28384  usgreghash2spot  28385  sbcoreleleqVD  28898  csbxpgVD  28933  sineq0ALT  28976  bnj607  29214  bnj1145  29289  bnj1204  29308  dvelimvNEW7  29389  cbval2OLD7  29657  cbvex2OLD7  29658  lssatle  29740  4atexlemex4  30797
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