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  1994  cbval2  2054  cbvex2  2055  2moswap  2329  2eu2  2335  pm2.61ne  2642  r19.21be  2767  uneqdifeq  3676  ssunsn2  3918  ssuni  3997  uniss2  4006  elpwuni  4138  elssabg  4315  elpw2g  4323  oteqex  4409  epelg  4455  wereu  4538  ordtr2  4585  ordsssuc2  4629  difex2  4673  ordpwsuc  4754  ordsucun  4764  limuni3  4791  ordom  4813  relop  4982  riinint  5085  sotri3  5223  unixpid  5363  cnviin  5368  funopg  5444  fun  5566  tz6.12c  5709  fvmptnf  5781  eldmrexrnb  5836  fmptco  5860  fnressn  5877  fressnfv  5879  fvtp2g  5902  fvtp3g  5903  fconst2g  5905  isores3  6014  isoselem  6020  eloprabga  6119  fo1stres  6329  poxp  6417  soxp  6418  brtpos2  6444  sorpsscmpl  6492  onnseq  6565  smores  6573  smofvon2  6577  oacl  6738  omcl  6739  oecl  6740  oawordri  6752  oalimcl  6762  oaass  6763  oarec  6764  omwordri  6774  omeulem1  6784  omeulem2  6785  oeordi  6789  oeworde  6795  oeoelem  6800  nnacl  6813  nnmcl  6814  nnecl  6815  nnacom  6819  nnaass  6824  nnmsucr  6827  nnmordi  6833  omabs  6849  iiner  6935  th3qlem2  6970  elpmg  6991  pmss12g  6999  mapsn  7014  f1domg  7086  ssdomg  7112  domtriord  7212  php  7250  php3  7252  1sdom  7270  fisseneq  7279  isinf  7281  ssnnfi  7287  dif1enOLD  7299  dif1en  7300  findcard3  7309  frfi  7311  unfi  7333  difinf  7336  fnfi  7343  iunfi  7353  elfi2  7377  marypha1lem  7396  marypha1  7397  oiexg  7460  harword  7489  brwdom  7491  unxpwdom  7513  inf3lemd  7538  inf3lem5  7543  cantnfval2  7580  cantnfle  7582  cantnflt  7583  cnfcom  7613  en3lplem1  7626  tcmin  7636  r1sdom  7656  rankxplim3  7761  cardidm  7802  cardmin2  7841  infxpenlem  7851  fseqenlem1  7861  numacn  7886  alephordi  7911  iscard3  7930  alephinit  7932  carduniima  7933  iunfictbso  7951  dfac5  7965  dfac12lem3  7981  pwsdompw  8040  pwcdadom  8052  cflim2  8099  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  alephsing  8112  infpssALT  8149  fin23lem34  8182  isf32lem2  8190  isf32lem10  8198  isf32lem12  8200  isfin1-2  8221  hsmexlem4  8265  axcc2lem  8272  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ac6num  8315  ac6s  8320  zorn2lem7  8338  ttukeylem5  8349  imadomg  8368  iundom2g  8371  ondomon  8394  ficard  8396  konigthlem  8399  alephreg  8413  pwcfsdom  8414  cfpwsdom  8415  axregndlem1  8433  axregnd  8435  pwfseqlem3  8491  pwxpndom2  8496  pwxpndom  8497  pwcdandom  8498  inawinalem  8520  gchina  8530  wuncval2  8578  tsk0  8594  tskxpss  8603  inatsk  8609  tskuni  8614  gruina  8649  grothac  8661  addclpi  8725  addnidpi  8734  nqereu  8762  mulcanenq  8793  genpnnp  8838  nqpr  8847  prlem934  8866  reclem2pr  8881  suplem1pr  8885  mulcmpblnr  8905  supsrlem  8942  axpre-sup  9000  1re  9046  00id  9197  receu  9623  sup3  9921  peano5nni  9959  nnaddcl  9978  zrevaddcl  10277  zdiv  10296  nneo  10309  zeo2  10312  fzind  10324  fnn0ind  10325  uzwo  10495  uzwoOLD  10496  lbzbi  10520  qrevaddcl  10552  irradd  10554  irrmul  10555  ltsubrp  10599  ltaddrp  10600  icoshft  10975  fzen  11028  elfzm11  11071  uzsplit  11073  injresinjlem  11154  injresinj  11155  om2uzlti  11245  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqcaopr3  11313  seqf1olem2a  11316  seqf1o  11319  seqid2  11324  seqhomo  11325  ser1const  11334  expadd  11377  expmul  11380  leexp1a  11393  faccl  11531  facdiv  11533  faclbnd  11536  faclbnd4lem4  11542  faclbnd6  11545  hasheqf1oi  11590  hashf1rn  11591  hashgadd  11606  hashdomi  11609  hashinfxadd  11614  hashunx  11615  hashunsng  11620  elprchashprn2  11622  hashle00  11624  hash1snb  11636  hashmap  11653  hashf1lem2  11660  hashf1  11661  seqcoll  11667  brfi1uzind  11670  sswrd  11692  shftlem  11838  caubnd  12117  rlimcld2  12327  o1dif  12378  climub  12410  climserle  12411  iseraltlem2  12431  sumss  12473  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  cvgrat  12615  sin01gt0  12746  ruclem8  12791  ruclem9  12792  dvds2ln  12835  dvdslelem  12849  alzdvds  12854  ndvdsadd  12883  bitsinv1  12909  sadcadd  12925  sadadd2  12927  saddisjlem  12931  smuval2  12949  smupvallem  12950  smu01lem  12952  smupval  12955  smueqlem  12957  smumullem  12959  gcddiv  13004  gcdmultiple  13005  rplpwr  13011  nn0seqcvgd  13016  seq1st  13017  alginv  13021  algcvga  13025  algfx  13026  isprm2  13042  isprm3  13043  prmind2  13045  maxprmfct  13068  prmdvdsexp  13069  pcmpt  13216  prmreclem4  13242  vdwmc2  13302  vdwlem10  13313  ramub2  13337  ramcl  13352  imasleval  13721  divsfval  13727  mreexexlem4d  13827  isssc  13975  istos  14419  frmdgsum  14762  mhmmulg  14877  resghm2b  14979  elsymgbas  15052  gsumwrev  15117  odlem1  15128  odcl2  15156  gexlem1  15168  sylow1lem1  15187  efgi2  15312  efginvrel2  15314  efgsrel  15321  cyggexb  15463  gsummulglem  15491  gsum2d  15501  dmdprd  15514  dprdw  15523  ablfac1eulem  15585  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  cnfldmulg  16688  cnfldexp  16689  obslbs  16912  fctop  17023  mretopd  17111  restopnb  17193  restdis  17196  tgcnp  17271  cncls2  17291  cncls  17292  cnntr  17293  cnsscnp  17297  cmpsub  17417  2ndcsep  17475  1stcelcls  17477  txcn  17611  txlm  17633  xkohaus  17638  qtopres  17683  haushmphlem  17772  cmphmph  17773  conhmph  17774  reghmph  17778  nrmhmph  17779  ptcmpfi  17798  reghaus  17810  fbssfi  17822  fbun  17825  fbfinnfr  17826  isfildlem  17842  fgcl  17863  cfinfil  17878  supfil  17880  ufinffr  17914  fin1aufil  17917  cnpflf  17986  alexsubALTlem3  18033  alexsubALT  18035  cnextfvval  18049  cnextcn  18051  tmdmulg  18075  tmdgsum  18078  tgphaus  18099  tgpt1  18100  mettri  18335  imasdsf1olem  18356  blssexps  18409  blssex  18410  mopni3  18477  metss  18491  metutopOLD  18565  psmetutop  18566  dscmet  18573  rectbntr0  18816  metnrmlem1a  18841  fsumcn  18853  lmmbr  19164  caubl  19213  caublcls  19214  bcthlem5  19234  bcth3  19237  ovolunlem1a  19345  ovoliunnul  19356  ovolicc2lem3  19368  finiunmbl  19391  voliunlem1  19397  volsuplem  19402  volsup  19403  dyadmax  19443  itgfsum  19671  dvnadd  19768  dvnres  19770  cpnord  19774  dvnfre  19791  dvmptfsum  19812  dvlip  19830  pf1ind  19928  fta1g  20043  plyco  20113  dgrcolem1  20144  dgrco  20146  dvnply2  20157  plydivex  20167  plyexmo  20183  aannenlem1  20198  aaliou3lem2  20213  dvntaylp  20240  taylthlem1  20242  ulmval  20249  cxpmul2  20533  scvxcvx  20777  jensenlem2  20779  jensen  20780  ppiub  20941  bcmono  21014  bpos1lem  21019  bposlem5  21025  lgsquad2lem2  21096  dchrisumlem1  21136  dchrisum0flb  21157  pntpbnd1  21233  pntlemf  21252  qabvle  21272  qabvexp  21273  ostthlem2  21275  ostth2lem2  21281  usgraedgprv  21349  usgranloopv  21351  usgraidx2vlem2  21364  usgrafisbase  21381  edgusgranbfin  21412  nb3graprlem2  21414  cusgra2v  21424  cusgrafi  21444  sizeusglecusglem1  21446  sizeusglecusg  21448  usgramaxsize  21449  2trllemH  21505  2trllemE  21506  usgrnloop  21516  spthonepeq  21540  wlkdvspthlem  21560  wlkdvspth  21561  cyclnspth  21571  fargshiftf  21576  fargshiftf1  21577  3v3e3cycl2  21604  3v3e3cycl  21605  4cycl4dv  21607  iseupa  21640  eupatrl  21643  eupath2  21655  elghomlem2  21903  isrngo  21919  rngodm1dm2  21959  rngoridfz  21976  hlim2  22647  elnlfn  23384  stle0i  23695  hstrbi  23722  spansncv2  23749  h1da  23805  fmptcof2  24029  xreceu  24121  tpr2rico  24263  hasheuni  24428  ismeas  24506  rrvsum  24665  dstfrvunirn  24685  subfacp1lem6  24824  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem12  24954  cvmlift3lem4  24962  ghomf1olem  25058  climuzcnv  25061  relexpsucr  25083  relexpsucl  25085  relexpcnv  25086  relexprel  25087  relexpdm  25088  relexprn  25089  relexpfld  25090  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  rtrclreclem.min  25100  rtrclind  25102  dedekindle  25141  clim2prod  25169  prodfn0  25175  prodfrec  25176  ntrivcvg  25178  prodmo  25215  fprodss  25227  fprodabs  25250  fprodefsum  25251  fprodn0  25256  fprod2d  25258  iprodefisumlem  25270  fprb  25343  dfon2lem9  25361  trpredtr  25447  trpredmintr  25448  dftrpred3g  25450  trpredrec  25455  soseq  25468  wfrlem12  25481  frrlem11  25507  sltval2  25524  sltsolem1  25536  axeuclidlem  25805  axcontlem12  25818  linethru  25991  elhf2  26020  hfext  26028  nndivsub  26111  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  finminlem  26211  fnessref  26263  lfinpfin  26273  locfincmp  26274  comppfsc  26277  neibastop2lem  26279  fnemeet2  26286  cover2  26305  upixp  26321  sdclem2  26336  fdc  26339  seqpo  26341  metf1o  26351  mettrifi  26353  sstotbnd3  26375  heibor1lem  26408  heiborlem5  26414  heibor  26420  bfplem1  26421  grpokerinj  26450  ispridl2  26538  mzpsubst  26695  jm2.18  26949  wepwsolem  27006  stoweidlem2  27618  stoweidlem17  27633  stoweidlem21  27637  2reu2  27832  afveu  27884  funbrafv  27889  ndmaovass  27937  euhash1  27998  swrd0  28002  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin12lem3  28024  swrdccat3b  28031  usgra2wlkspthlem1  28036  usgra2wlkspthlem2  28037  2wlkonot3v  28072  2spthonot3v  28073  usg2wlkonot  28080  usg2wotspth  28081  usgfidegfi  28090  frgra2v  28103  frgra3vlem1  28104  3vfriswmgra  28109  1to2vfriswmgra  28110  1to3vfriswmgra  28111  2pthfrgra  28115  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  3cyclfrgrarn2  28118  4cycl2vnunb  28121  vdn0frgrav2  28128  vdgn0frgrav2  28129  frgrancvvdeqlem4  28136  frgrancvvdeqlemB  28141  frgrancvvdeqlemC  28142  frgrawopreglem2  28148  frgrawopreglem4  28150  frgrawopreg  28152  frgraregorufr0  28155  frgraeu  28157  frg2woteqm  28162  2spotmdisj  28171  usgreghash2spot  28172  sbcoreleleqVD  28680  csbxpgVD  28715  bnj607  28993  bnj1145  29068  bnj1204  29087  dvelimvNEW7  29168  cbval2OLD7  29414  cbvex2OLD7  29415  lssatle  29498  4atexlemex4  30555
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