MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expcom 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  dvelimvOLD  1985  cbval2  2038  cbvex2  2039  2moswap  2313  2eu2  2319  pm2.61ne  2625  r19.21be  2750  uneqdifeq  3659  ssunsn2  3901  ssuni  3979  uniss2  3988  elpwuni  4119  elssabg  4296  elpw2g  4304  oteqex  4390  epelg  4436  wereu  4519  ordtr2  4566  ordsssuc2  4610  difex2  4654  ordpwsuc  4735  ordsucun  4745  limuni3  4772  ordom  4794  relop  4963  riinint  5066  sotri3  5204  unixpid  5344  cnviin  5349  funopg  5425  fun  5547  tz6.12c  5690  fvmptnf  5761  eldmrexrnb  5816  fmptco  5840  fnressn  5857  fressnfv  5859  fvtp2g  5882  fvtp3g  5883  fconst2g  5885  isores3  5994  isoselem  6000  eloprabga  6099  fo1stres  6309  poxp  6394  soxp  6395  brtpos2  6421  sorpsscmpl  6469  onnseq  6542  smores  6550  smofvon2  6554  oacl  6715  omcl  6716  oecl  6717  oawordri  6729  oalimcl  6739  oaass  6740  oarec  6741  omwordri  6751  omeulem1  6761  omeulem2  6762  oeordi  6766  oeworde  6772  oeoelem  6777  nnacl  6790  nnmcl  6791  nnecl  6792  nnacom  6796  nnaass  6801  nnmsucr  6804  nnmordi  6810  omabs  6826  iiner  6912  th3qlem2  6947  elpmg  6968  pmss12g  6976  mapsn  6991  f1domg  7063  ssdomg  7089  domtriord  7189  php  7227  php3  7229  1sdom  7247  fisseneq  7256  isinf  7258  ssnnfi  7264  dif1enOLD  7276  dif1en  7277  findcard3  7286  frfi  7288  unfi  7310  difinf  7313  fnfi  7320  iunfi  7330  elfi2  7354  marypha1lem  7373  marypha1  7374  oiexg  7437  harword  7466  brwdom  7468  unxpwdom  7490  inf3lemd  7515  inf3lem5  7520  cantnfval2  7557  cantnfle  7559  cantnflt  7560  cnfcom  7590  en3lplem1  7603  tcmin  7613  r1sdom  7633  rankxplim3  7738  cardidm  7779  cardmin2  7818  infxpenlem  7828  fseqenlem1  7838  numacn  7863  alephordi  7888  iscard3  7907  alephinit  7909  carduniima  7910  iunfictbso  7928  dfac5  7942  dfac12lem3  7958  pwsdompw  8017  pwcdadom  8029  cflim2  8076  cfslb2n  8081  cofsmo  8082  cfsmolem  8083  cfcoflem  8085  alephsing  8089  infpssALT  8126  fin23lem34  8159  isf32lem2  8167  isf32lem10  8175  isf32lem12  8177  isfin1-2  8198  hsmexlem4  8242  axcc2lem  8249  domtriomlem  8255  axdc2lem  8261  axdc3lem2  8264  axdc3lem4  8266  axdc4lem  8268  axcclem  8270  ac6num  8292  ac6s  8297  zorn2lem7  8315  ttukeylem5  8326  imadomg  8345  iundom2g  8348  ondomon  8371  ficard  8373  konigthlem  8376  alephreg  8390  pwcfsdom  8391  cfpwsdom  8392  axregndlem1  8410  axregnd  8412  pwfseqlem3  8468  pwxpndom2  8473  pwxpndom  8474  pwcdandom  8475  inawinalem  8497  gchina  8507  wuncval2  8555  tsk0  8571  tskxpss  8580  inatsk  8586  tskuni  8591  gruina  8626  grothac  8638  addclpi  8702  addnidpi  8711  nqereu  8739  mulcanenq  8770  genpnnp  8815  nqpr  8824  prlem934  8843  reclem2pr  8858  suplem1pr  8862  mulcmpblnr  8882  supsrlem  8919  axpre-sup  8977  1re  9023  00id  9173  receu  9599  sup3  9897  peano5nni  9935  nnaddcl  9954  zrevaddcl  10253  zdiv  10272  nneo  10285  zeo2  10288  fzind  10300  fnn0ind  10301  uzwo  10471  uzwoOLD  10472  lbzbi  10496  qrevaddcl  10528  irradd  10530  irrmul  10531  ltsubrp  10575  ltaddrp  10576  icoshft  10951  fzen  11004  elfzm11  11046  uzsplit  11048  injresinjlem  11126  injresinj  11127  om2uzlti  11217  seqcl2  11268  seqfveq2  11272  seqshft2  11276  monoord  11280  seqsplit  11283  seqcaopr3  11285  seqf1olem2a  11288  seqf1o  11291  seqid2  11296  seqhomo  11297  ser1const  11306  expadd  11349  expmul  11352  leexp1a  11365  faccl  11503  facdiv  11505  faclbnd  11508  faclbnd4lem4  11514  faclbnd6  11517  hasheqf1oi  11562  hashgadd  11578  hashdomi  11581  hashinfxadd  11586  hashunx  11587  hashunsng  11592  elprchashprn2  11594  hashle00  11596  hash1snb  11608  hashmap  11625  hashf1lem2  11632  hashf1  11633  seqcoll  11639  brfi1uzind  11642  sswrd  11664  shftlem  11810  caubnd  12089  rlimcld2  12299  o1dif  12350  climub  12382  climserle  12383  iseraltlem2  12403  sumss  12445  fsum2d  12482  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  bcxmas  12542  climcndslem1  12556  climcndslem2  12557  cvgrat  12587  sin01gt0  12718  ruclem8  12763  ruclem9  12764  dvds2ln  12807  dvdslelem  12821  alzdvds  12826  ndvdsadd  12855  bitsinv1  12881  sadcadd  12897  sadadd2  12899  saddisjlem  12903  smuval2  12921  smupvallem  12922  smu01lem  12924  smupval  12927  smueqlem  12929  smumullem  12931  gcddiv  12976  gcdmultiple  12977  rplpwr  12983  nn0seqcvgd  12988  seq1st  12989  alginv  12993  algcvga  12997  algfx  12998  isprm2  13014  isprm3  13015  prmind2  13017  maxprmfct  13040  prmdvdsexp  13041  pcmpt  13188  prmreclem4  13214  vdwmc2  13274  vdwlem10  13285  ramub2  13309  ramcl  13324  imasleval  13693  divsfval  13699  mreexexlem4d  13799  isssc  13947  istos  14391  frmdgsum  14734  mhmmulg  14849  resghm2b  14951  elsymgbas  15024  gsumwrev  15089  odlem1  15100  odcl2  15128  gexlem1  15140  sylow1lem1  15159  efgi2  15284  efginvrel2  15286  efgsrel  15293  cyggexb  15435  gsummulglem  15463  gsum2d  15473  dmdprd  15486  dprdw  15495  ablfac1eulem  15557  mplcoe1  16455  mplcoe3  16456  mplcoe2  16457  cnfldmulg  16656  cnfldexp  16657  obslbs  16880  fctop  16991  mretopd  17079  restopnb  17161  restdis  17164  tgcnp  17239  cncls2  17259  cncls  17260  cnntr  17261  cnsscnp  17265  cmpsub  17385  2ndcsep  17443  1stcelcls  17445  txcn  17579  txlm  17601  xkohaus  17606  qtopres  17651  haushmphlem  17740  cmphmph  17741  conhmph  17742  reghmph  17746  nrmhmph  17747  ptcmpfi  17766  reghaus  17778  fbssfi  17790  fbun  17793  fbfinnfr  17794  isfildlem  17810  fgcl  17831  cfinfil  17846  supfil  17848  ufinffr  17882  fin1aufil  17885  cnpflf  17954  alexsubALTlem3  18001  alexsubALT  18003  cnextfvval  18017  cnextcn  18019  tmdmulg  18043  tmdgsum  18046  tgphaus  18067  tgpt1  18068  mettri  18290  imasdsf1olem  18311  blssex  18347  mopni3  18414  metss  18428  metutop  18487  dscmet  18491  rectbntr0  18734  metnrmlem1a  18759  fsumcn  18771  lmmbr  19082  caubl  19131  caublcls  19132  bcthlem5  19150  bcth3  19153  ovolunlem1a  19259  ovoliunnul  19270  ovolicc2lem3  19282  finiunmbl  19305  voliunlem1  19311  volsuplem  19316  volsup  19317  dyadmax  19357  itgfsum  19585  dvnadd  19682  dvnres  19684  cpnord  19688  dvnfre  19705  dvmptfsum  19726  dvlip  19744  pf1ind  19842  fta1g  19957  plyco  20027  dgrcolem1  20058  dgrco  20060  dvnply2  20071  plydivex  20081  plyexmo  20097  aannenlem1  20112  aaliou3lem2  20127  dvntaylp  20154  taylthlem1  20156  ulmval  20163  cxpmul2  20447  scvxcvx  20691  jensenlem2  20693  jensen  20694  ppiub  20855  bcmono  20928  bpos1lem  20933  bposlem5  20939  lgsquad2lem2  21010  dchrisumlem1  21050  dchrisum0flb  21071  pntpbnd1  21147  pntlemf  21166  qabvle  21186  qabvexp  21187  ostthlem2  21189  ostth2lem2  21195  usgraedgprv  21263  usgraidx2vlem2  21277  usgrafisbase  21294  edgusgranbfin  21325  nb3graprlem2  21327  cusgra2v  21337  cusgrafi  21357  sizeusglecusglem1  21359  sizeusglecusg  21361  usgramaxsize  21362  usgrnloop  21419  constr2trl  21446  wlkdvspthlem  21455  wlkdvspth  21456  cyclnspth  21466  fargshiftf  21471  fargshiftf1  21472  3v3e3cycl2  21499  3v3e3cycl  21500  4cycl4dv  21502  iseupa  21535  eupatrl  21538  eupath2  21550  elghomlem2  21798  isrngo  21814  rngodm1dm2  21854  rngoridfz  21871  hlim2  22542  elnlfn  23279  stle0i  23590  hstrbi  23617  spansncv2  23644  h1da  23700  fmptcof2  23918  xreceu  24006  tpr2rico  24114  hasheuni  24271  ismeas  24349  rrvsum  24491  dstfrvunirn  24511  subfacp1lem6  24650  cvmliftlem7  24757  cvmliftlem10  24760  cvmlift2lem12  24780  cvmlift3lem4  24788  ghomf1olem  24884  climuzcnv  24887  relexpsucr  24909  relexpsucl  24911  relexpcnv  24912  relexprel  24913  relexpdm  24914  relexprn  24915  relexpfld  24916  relexpadd  24917  relexpindlem  24918  rtrclreclem.trans  24925  rtrclreclem.min  24926  rtrclind  24928  dedekindle  24967  clim2prod  24995  prodfn0  25001  prodfrec  25002  ntrivcvg  25004  prodmo  25041  fprodss  25053  fprodabs  25076  fprodefsum  25077  fprodn0  25082  fprb  25153  dfon2lem9  25171  trpredtr  25257  trpredmintr  25258  dftrpred3g  25260  trpredrec  25265  soseq  25278  wfrlem12  25291  frrlem11  25317  sltval2  25334  sltsolem1  25346  axeuclidlem  25615  axcontlem12  25628  linethru  25801  elhf2  25830  hfext  25838  nndivsub  25921  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  finminlem  26012  fnessref  26064  lfinpfin  26074  locfincmp  26075  comppfsc  26078  neibastop2lem  26080  fnemeet2  26087  cover2  26106  upixp  26122  sdclem2  26137  fdc  26140  seqpo  26142  metf1o  26152  mettrifi  26154  sstotbnd3  26176  heibor1lem  26209  heiborlem5  26215  heibor  26221  bfplem1  26222  grpokerinj  26251  ispridl2  26339  mzpsubst  26496  jm2.18  26750  wepwsolem  26807  stoweidlem2  27419  stoweidlem17  27434  stoweidlem21  27438  2reu2  27633  afveu  27686  funbrafv  27691  ndmaovass  27739  frgra2v  27752  frgra3vlem1  27753  3vfriswmgra  27758  1to2vfriswmgra  27759  1to3vfriswmgra  27760  2pthfrgra  27764  3cyclfrgrarn1  27765  3cyclfrgrarn  27766  3cyclfrgrarn2  27767  4cycl2vnunb  27770  vdn0frgrav2  27777  vdgn0frgrav2  27778  frgrancvvdeqlem4  27785  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  frgrawopreglem2  27797  frgrawopreglem4  27799  frgrawopreg  27801  frgraregorufr0  27804  sbcoreleleqVD  28312  csbxpgVD  28347  bnj607  28625  bnj1145  28700  bnj1204  28719  dvelimvNEW7  28800  cbval2OLD7  29046  cbvex2OLD7  29047  lssatle  29130  4atexlemex4  30187
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