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

Theorem expcom 426
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 425 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ancoms  441  syldan  458  sylan  459  4casesdan  918  dedlema  922  dedlemb  923  cbval2  1992  cbval2OLD  1993  cbvex2  1994  dvelimvOLD  2031  2moswap  2362  2eu2  2368  pm2.61ne  2685  r19.21be  2813  uneqdifeq  3740  ssunsn2  3982  ssuni  4061  uniss2  4070  elpwuni  4203  elssabg  4384  elpw2g  4392  oteqex  4478  epelg  4524  wereu  4607  ordtr2  4654  ordsssuc2  4699  difex2  4743  ordpwsuc  4824  ordsucun  4834  limuni3  4861  ordom  4883  relop  5052  riinint  5155  sotri3  5293  unixpid  5433  cnviin  5438  funopg  5514  fun  5636  tz6.12c  5779  fvmptnf  5851  eldmrexrnb  5906  fmptco  5930  fnressn  5947  fressnfv  5949  fvtp2g  5972  fvtp3g  5973  fconst2g  5975  isores3  6084  isoselem  6090  eloprabga  6189  fo1stres  6399  poxp  6487  soxp  6488  brtpos2  6514  sorpsscmpl  6562  onnseq  6635  smores  6643  smofvon2  6647  oacl  6808  omcl  6809  oecl  6810  oawordri  6822  oalimcl  6832  oaass  6833  oarec  6834  omwordri  6844  omeulem1  6854  omeulem2  6855  oeordi  6859  oeworde  6865  oeoelem  6870  nnacl  6883  nnmcl  6884  nnecl  6885  nnacom  6889  nnaass  6894  nnmsucr  6897  nnmordi  6903  omabs  6919  iiner  7005  th3qlem2  7040  elpmg  7061  pmss12g  7069  mapsn  7084  f1domg  7156  ssdomg  7182  domtriord  7282  php  7320  php3  7322  1sdom  7340  fisseneq  7349  isinf  7351  ssnnfi  7357  dif1enOLD  7369  dif1en  7370  findcard3  7379  frfi  7381  unfi  7403  difinf  7406  fnfi  7413  iunfi  7423  elfi2  7448  marypha1lem  7467  marypha1  7468  oiexg  7533  harword  7562  brwdom  7564  unxpwdom  7586  inf3lemd  7611  inf3lem5  7616  cantnfval2  7653  cantnfle  7655  cantnflt  7656  cnfcom  7686  en3lplem1  7699  tcmin  7709  r1sdom  7729  rankxplim3  7836  cardidm  7877  cardmin2  7916  infxpenlem  7926  fseqenlem1  7936  numacn  7961  alephordi  7986  iscard3  8005  alephinit  8007  carduniima  8008  iunfictbso  8026  dfac5  8040  dfac12lem3  8056  pwsdompw  8115  pwcdadom  8127  cflim2  8174  cfslb2n  8179  cofsmo  8180  cfsmolem  8181  cfcoflem  8183  alephsing  8187  infpssALT  8224  fin23lem34  8257  isf32lem2  8265  isf32lem10  8273  isf32lem12  8275  isfin1-2  8296  hsmexlem4  8340  axcc2lem  8347  domtriomlem  8353  axdc2lem  8359  axdc3lem2  8362  axdc3lem4  8364  axdc4lem  8366  axcclem  8368  ac6num  8390  ac6s  8395  zorn2lem7  8413  ttukeylem5  8424  imadomg  8443  iundom2g  8446  ondomon  8469  ficard  8471  konigthlem  8474  alephreg  8488  pwcfsdom  8489  cfpwsdom  8490  axregndlem1  8508  axregnd  8510  pwfseqlem3  8566  pwxpndom2  8571  pwxpndom  8572  pwcdandom  8573  inawinalem  8595  gchina  8605  wuncval2  8653  tsk0  8669  tskxpss  8678  inatsk  8684  tskuni  8689  gruina  8724  grothac  8736  addclpi  8800  addnidpi  8809  nqereu  8837  mulcanenq  8868  genpnnp  8913  nqpr  8922  prlem934  8941  reclem2pr  8956  suplem1pr  8960  mulcmpblnr  8980  supsrlem  9017  axpre-sup  9075  1re  9121  00id  9272  receu  9698  sup3  9996  peano5nni  10034  nnaddcl  10053  zrevaddcl  10352  zdiv  10371  nneo  10384  zeo2  10387  fzind  10399  fnn0ind  10400  uzwo  10570  uzwoOLD  10571  lbzbi  10595  qrevaddcl  10627  irradd  10629  irrmul  10630  ltsubrp  10674  ltaddrp  10675  icoshft  11050  fzen  11103  elfzm11  11147  uzsplit  11149  injresinjlem  11230  injresinj  11231  om2uzlti  11321  seqcl2  11372  seqfveq2  11376  seqshft2  11380  monoord  11384  seqsplit  11387  seqcaopr3  11389  seqf1olem2a  11392  seqf1o  11395  seqid2  11400  seqhomo  11401  ser1const  11410  expadd  11453  expmul  11456  leexp1a  11469  faccl  11607  facdiv  11609  faclbnd  11612  faclbnd4lem4  11618  faclbnd6  11621  hasheqf1oi  11666  hashf1rn  11667  hashgadd  11682  hashdomi  11685  hashinfxadd  11690  hashunx  11691  hashunsng  11696  elprchashprn2  11698  hashle00  11700  hash1snb  11712  hashmap  11729  hashf1lem2  11736  hashf1  11737  seqcoll  11743  brfi1uzind  11746  sswrd  11768  shftlem  11914  caubnd  12193  rlimcld2  12403  o1dif  12454  climub  12486  climserle  12487  iseraltlem2  12507  sumss  12549  fsum2d  12586  fsumabs  12611  fsumrlim  12621  fsumo1  12622  fsumiun  12631  bcxmas  12646  climcndslem1  12660  climcndslem2  12661  cvgrat  12691  sin01gt0  12822  ruclem8  12867  ruclem9  12868  dvds2ln  12911  dvdslelem  12925  alzdvds  12930  ndvdsadd  12959  bitsinv1  12985  sadcadd  13001  sadadd2  13003  saddisjlem  13007  smuval2  13025  smupvallem  13026  smu01lem  13028  smupval  13031  smueqlem  13033  smumullem  13035  gcddiv  13080  gcdmultiple  13081  rplpwr  13087  nn0seqcvgd  13092  seq1st  13093  alginv  13097  algcvga  13101  algfx  13102  isprm2  13118  isprm3  13119  prmind2  13121  maxprmfct  13144  prmdvdsexp  13145  pcmpt  13292  prmreclem4  13318  vdwmc2  13378  vdwlem10  13389  ramub2  13413  ramcl  13428  imasleval  13797  divsfval  13803  mreexexlem4d  13903  isssc  14051  istos  14495  frmdgsum  14838  mhmmulg  14953  resghm2b  15055  elsymgbas  15128  gsumwrev  15193  odlem1  15204  odcl2  15232  gexlem1  15244  sylow1lem1  15263  efgi2  15388  efginvrel2  15390  efgsrel  15397  cyggexb  15539  gsummulglem  15567  gsum2d  15577  dmdprd  15590  dprdw  15599  ablfac1eulem  15661  mplcoe1  16559  mplcoe3  16560  mplcoe2  16561  cnfldmulg  16764  cnfldexp  16765  obslbs  16988  fctop  17099  mretopd  17187  restopnb  17270  restdis  17273  tgcnp  17348  cncls2  17368  cncls  17369  cnntr  17370  cnsscnp  17374  cmpsub  17494  2ndcsep  17553  1stcelcls  17555  txcn  17689  txlm  17711  xkohaus  17716  qtopres  17761  haushmphlem  17850  cmphmph  17851  conhmph  17852  reghmph  17856  nrmhmph  17857  ptcmpfi  17876  reghaus  17888  fbssfi  17900  fbun  17903  fbfinnfr  17904  isfildlem  17920  fgcl  17941  cfinfil  17956  supfil  17958  ufinffr  17992  fin1aufil  17995  cnpflf  18064  alexsubALTlem3  18111  alexsubALT  18113  cnextfvval  18127  cnextcn  18129  tmdmulg  18153  tmdgsum  18156  tgphaus  18177  tgpt1  18178  mettri  18413  imasdsf1olem  18434  blssexps  18487  blssex  18488  mopni3  18555  metss  18569  metutopOLD  18643  psmetutop  18644  dscmet  18651  rectbntr0  18894  metnrmlem1a  18919  fsumcn  18931  lmmbr  19242  caubl  19291  caublcls  19292  bcthlem5  19312  bcth3  19315  ovolunlem1a  19423  ovoliunnul  19434  ovolicc2lem3  19446  finiunmbl  19469  voliunlem1  19475  volsuplem  19480  volsup  19481  dyadmax  19521  itgfsum  19747  dvnadd  19846  dvnres  19848  cpnord  19852  dvnfre  19869  dvmptfsum  19890  dvlip  19908  pf1ind  20006  fta1g  20121  plyco  20191  dgrcolem1  20222  dgrco  20224  dvnply2  20235  plydivex  20245  plyexmo  20261  aannenlem1  20276  aaliou3lem2  20291  dvntaylp  20318  taylthlem1  20320  ulmval  20327  cxpmul2  20611  scvxcvx  20855  jensenlem2  20857  jensen  20858  ppiub  21019  bcmono  21092  bpos1lem  21097  bposlem5  21103  lgsquad2lem2  21174  dchrisumlem1  21214  dchrisum0flb  21235  pntpbnd1  21311  pntlemf  21330  qabvle  21350  qabvexp  21351  ostthlem2  21353  ostth2lem2  21359  usgraedgprv  21427  usgranloopv  21429  usgraidx2vlem2  21442  usgrafisbase  21459  edgusgranbfin  21490  nb3graprlem2  21492  cusgra2v  21502  cusgrafi  21522  sizeusglecusglem1  21524  sizeusglecusg  21526  usgramaxsize  21527  2trllemH  21583  2trllemE  21584  usgrnloop  21594  spthonepeq  21618  wlkdvspthlem  21638  wlkdvspth  21639  cyclnspth  21649  fargshiftf  21654  fargshiftf1  21655  3v3e3cycl2  21682  3v3e3cycl  21683  4cycl4dv  21685  iseupa  21718  eupatrl  21721  eupath2  21733  elghomlem2  21981  isrngo  21997  rngodm1dm2  22037  rngoridfz  22054  hlim2  22725  elnlfn  23462  stle0i  23773  hstrbi  23800  spansncv2  23827  h1da  23883  fmptcof2  24107  xreceu  24199  tpr2rico  24341  hasheuni  24506  ismeas  24584  rrvsum  24743  dstfrvunirn  24763  subfacp1lem6  24902  cvmliftlem7  25009  cvmliftlem10  25012  cvmlift2lem12  25032  cvmlift3lem4  25040  ghomf1olem  25136  climuzcnv  25139  relexpsucr  25161  relexpsucl  25163  relexpcnv  25164  relexprel  25165  relexpdm  25166  relexprn  25167  relexpfld  25168  relexpadd  25169  relexpindlem  25170  rtrclreclem.trans  25177  rtrclreclem.min  25178  rtrclind  25180  dedekindle  25219  clim2prod  25247  prodfn0  25253  prodfrec  25254  ntrivcvg  25256  prodmo  25293  fprodss  25305  fprodabs  25328  fprodefsum  25329  fprodn0  25334  fprod2d  25336  iprodefisumlem  25348  fprb  25428  dfon2lem9  25449  trpredtr  25539  trpredmintr  25540  dftrpred3g  25542  trpredrec  25547  soseq  25560  wfrlem12  25580  frrlem11  25625  sltval2  25642  sltsolem1  25654  axeuclidlem  25932  axcontlem12  25945  linethru  26118  elhf2  26147  hfext  26155  nndivsub  26238  wl-exeq  26265  heicant  26277  ovoliunnfl  26284  voliunnfl  26286  volsupnfl  26287  finminlem  26359  fnessref  26411  lfinpfin  26421  locfincmp  26422  comppfsc  26425  neibastop2lem  26427  fnemeet2  26434  cover2  26453  upixp  26469  sdclem2  26484  fdc  26487  seqpo  26489  metf1o  26499  mettrifi  26501  sstotbnd3  26523  heibor1lem  26556  heiborlem5  26562  heibor  26568  bfplem1  26569  grpokerinj  26598  ispridl2  26686  mzpsubst  26843  jm2.18  27097  wepwsolem  27154  stoweidlem2  27765  stoweidlem17  27780  stoweidlem21  27784  2reu2  27979  afveu  28031  funbrafv  28036  ndmaovass  28084  oprabv  28127  2elfz2melfz  28164  fzoopth  28186  modifeq2int  28208  euhash1  28214  hashss  28216  swrd0  28241  swrdvalodm2  28246  swrdvalodm  28247  swrd0swrd  28255  swrdswrdlem  28256  swrdswrd  28257  swrdccatin1  28263  swrdccatin2  28268  swrdccatin12lem3  28270  swrdccat3  28273  cshwcl  28298  cshwidx  28300  2cshw1lem1  28306  2cshw1lem2  28307  2cshw2lem2  28311  2cshw2lem3  28312  2cshwmod  28315  cshweqdif2s  28329  cshweqrep  28332  cshwssizelem4  28342  iswlkg  28362  usg2wlkeq  28366  usgra2wlkspthlem1  28368  usgra2wlkspthlem2  28369  wwlkn0  28395  2wlkonot3v  28431  2spthonot3v  28432  usg2wlkonot  28439  usg2wotspth  28440  usgfidegfi  28449  vdiscusgra  28459  cusgraisrusgra  28473  frgra2v  28487  frgra3vlem1  28488  3vfriswmgra  28493  1to2vfriswmgra  28494  1to3vfriswmgra  28495  2pthfrgra  28499  3cyclfrgrarn1  28500  3cyclfrgrarn  28501  3cyclfrgrarn2  28502  4cycl2vnunb  28505  vdn0frgrav2  28512  vdgn0frgrav2  28513  frgrancvvdeqlem4  28520  frgrancvvdeqlemB  28525  frgrancvvdeqlemC  28526  frgrawopreglem2  28532  frgrawopreglem4  28534  frgrawopreg  28536  frgraregorufr0  28539  frgraeu  28541  frg2woteqm  28546  2spotmdisj  28555  usgreghash2spot  28556  sbcoreleleqVD  29069  csbxpgVD  29104  sineq0ALT  29147  bnj607  29385  bnj1145  29460  bnj1204  29479  dvelimvNEW7  29560  cbval2OLD7  29828  cbvex2OLD7  29829  lssatle  29911  4atexlemex4  30968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator