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

Theorem expcom 424
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 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 27 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ancoms  439  syldan  456  sylan  457  4casesdan  916  dedlema  920  dedlemb  921  dvelimv  1881  cbval2  1946  cbvex2  1947  2moswap  2220  2mos  2224  2eu2  2226  pm2.61ne  2523  r19.21be  2646  uneqdifeq  3544  ssunsn2  3775  ssuni  3851  uniss2  3860  elpwuni  3991  elssabg  4168  elpw2g  4176  oteqex  4261  epelg  4308  wereu  4391  ordtr2  4438  ordsssuc2  4483  difex2  4527  ordpwsuc  4608  ordsucun  4618  limuni3  4645  ordom  4667  relop  4836  riinint  4937  sotri3  5075  unixpid  5209  cnviin  5214  funopg  5288  fun  5407  tz6.12c  5549  fvmptnf  5619  fmptco  5693  fnressn  5707  fressnfv  5709  fconst2g  5730  isores3  5834  isoselem  5840  eloprabga  5936  fo1stres  6145  poxp  6229  soxp  6230  brtpos2  6242  sorpsscmpl  6290  onnseq  6363  smores  6371  smofvon2  6375  oacl  6536  omcl  6537  oecl  6538  oawordri  6550  oalimcl  6560  oaass  6561  oarec  6562  omwordri  6572  omeulem1  6582  omeulem2  6583  oeordi  6587  oeworde  6593  oeoelem  6598  nnacl  6611  nnmcl  6612  nnecl  6613  nnacom  6617  nnaass  6622  nnmsucr  6625  nnmordi  6631  omabs  6647  iiner  6733  th3qlem2  6767  elpmg  6788  pmss12g  6796  mapsn  6811  f1domg  6883  ssdomg  6909  domtriord  7009  php  7047  php3  7049  1sdom  7067  fisseneq  7076  isinf  7078  ssnnfi  7084  dif1enOLD  7092  dif1en  7093  findcard3  7102  frfi  7104  unfi  7126  difinf  7129  fnfi  7136  iunfi  7146  elfi2  7170  marypha1lem  7188  marypha1  7189  oiexg  7252  harword  7281  brwdom  7283  unxpwdom  7305  inf3lemd  7330  inf3lem5  7335  cantnfval2  7372  cantnfle  7374  cantnflt  7375  cnfcom  7405  en3lplem1  7418  tcmin  7428  r1sdom  7448  rankxplim3  7553  cardidm  7594  cardmin2  7633  infxpenlem  7643  fseqenlem1  7653  numacn  7678  alephordi  7703  iscard3  7722  alephinit  7724  carduniima  7725  iunfictbso  7743  dfac5  7757  dfac12lem3  7773  pwsdompw  7832  pwcdadom  7844  cflim2  7891  cfslb2n  7896  cofsmo  7897  cfsmolem  7898  cfcoflem  7900  alephsing  7904  infpssALT  7941  fin23lem34  7974  isf32lem2  7982  isf32lem10  7990  isf32lem12  7992  isfin1-2  8013  hsmexlem4  8057  axcc2lem  8064  domtriomlem  8070  axdc2lem  8076  axdc3lem2  8079  axdc3lem4  8081  axdc4lem  8083  axcclem  8085  ac6num  8108  ac6s  8113  zorn2lem7  8131  ttukeylem5  8142  imadomg  8161  iundom2g  8164  ondomon  8187  ficard  8189  konigthlem  8192  alephreg  8206  pwcfsdom  8207  cfpwsdom  8208  axregndlem1  8226  axregnd  8228  pwfseqlem3  8284  pwxpndom2  8289  pwxpndom  8290  pwcdandom  8291  inawinalem  8313  gchina  8323  wuncval2  8371  tsk0  8387  tskxpss  8396  inatsk  8402  tskuni  8407  gruina  8442  grothac  8454  addclpi  8518  addnidpi  8527  nqereu  8555  mulcanenq  8586  genpnnp  8631  nqpr  8640  prlem934  8659  reclem2pr  8674  suplem1pr  8678  mulcmpblnr  8698  supsrlem  8735  axpre-sup  8793  1re  8839  00id  8989  receu  9415  sup3  9713  peano5nni  9751  nnaddcl  9770  zrevaddcl  10065  zdiv  10084  nneo  10097  zeo2  10100  fzind  10112  fnn0ind  10113  uzwo  10283  uzwoOLD  10284  lbzbi  10308  qrevaddcl  10340  irradd  10342  irrmul  10343  ltsubrp  10387  ltaddrp  10388  icoshft  10760  fzen  10813  elfzm11  10855  uzsplit  10857  om2uzlti  11015  seqcl2  11066  seqfveq2  11070  seqshft2  11074  monoord  11078  seqsplit  11081  seqcaopr3  11083  seqf1olem2a  11086  seqf1o  11089  seqid2  11094  seqhomo  11095  ser1const  11104  expadd  11146  expmul  11149  leexp1a  11162  faccl  11300  facdiv  11302  faclbnd  11305  faclbnd4lem4  11311  faclbnd6  11314  hashgadd  11361  hashdomi  11364  hashunsng  11369  hashmap  11389  hashf1lem2  11396  hashf1  11397  seqcoll  11403  sswrd  11425  shftlem  11565  caubnd  11844  rlimcld2  12054  o1dif  12105  climub  12137  climserle  12138  iseraltlem2  12157  sumss  12199  fsum2d  12236  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  bcxmas  12296  climcndslem1  12310  climcndslem2  12311  cvgrat  12341  sin01gt0  12472  ruclem8  12517  ruclem9  12518  dvds2ln  12561  dvdslelem  12575  alzdvds  12580  ndvdsadd  12609  bitsinv1  12635  sadcadd  12651  sadadd2  12653  saddisjlem  12657  smuval2  12675  smupvallem  12676  smu01lem  12678  smupval  12681  smueqlem  12683  smumullem  12685  gcddiv  12730  gcdmultiple  12731  rplpwr  12737  nn0seqcvgd  12742  seq1st  12743  alginv  12747  algcvga  12751  algfx  12752  isprm2  12768  isprm3  12769  prmind2  12771  maxprmfct  12794  prmdvdsexp  12795  pcmpt  12942  prmreclem4  12968  vdwmc2  13028  vdwlem10  13039  ramub2  13063  ramcl  13078  imasleval  13445  divsfval  13451  mreexexlem4d  13551  isssc  13699  istos  14143  frmdgsum  14486  mhmmulg  14601  resghm2b  14703  elsymgbas  14776  gsumwrev  14841  odlem1  14852  odcl2  14880  gexlem1  14892  sylow1lem1  14911  efgi2  15036  efginvrel2  15038  efgsrel  15045  cyggexb  15187  gsummulglem  15215  gsum2d  15225  dmdprd  15238  dprdw  15247  ablfac1eulem  15309  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  cnfldmulg  16408  cnfldexp  16409  obslbs  16632  fctop  16743  mretopd  16831  restopnb  16908  restdis  16911  tgcnp  16985  cncls2  17004  cncls  17005  cnntr  17006  cnsscnp  17010  cmpsub  17129  2ndcsep  17187  1stcelcls  17189  txcn  17322  txlm  17344  xkohaus  17349  qtopres  17391  haushmphlem  17480  cmphmph  17481  conhmph  17482  reghmph  17486  nrmhmph  17487  ptcmpfi  17506  reghaus  17518  fbssfi  17534  fbun  17537  fbfinnfr  17538  isfildlem  17554  fgcl  17575  cfinfil  17590  supfil  17592  ufinffr  17626  fin1aufil  17629  cnpflf  17698  alexsubALTlem3  17745  alexsubALT  17747  tmdmulg  17777  tmdgsum  17780  tgphaus  17801  tgpt1  17802  mettri  17918  imasdsf1olem  17939  blssex  17975  mopni3  18042  metss  18056  dscmet  18097  rectbntr0  18339  metnrmlem1a  18364  fsumcn  18376  lmmbr  18686  caubl  18735  caublcls  18736  bcthlem5  18752  bcth3  18755  ovolunlem1a  18857  ovoliunnul  18868  ovolicc2lem3  18880  finiunmbl  18903  voliunlem1  18909  volsuplem  18914  volsup  18915  dyadmax  18955  itgfsum  19183  dvnadd  19280  dvnres  19282  cpnord  19286  dvnfre  19303  dvmptfsum  19324  dvlip  19342  pf1ind  19440  fta1g  19555  plyco  19625  dgrcolem1  19656  dgrco  19658  dvnply2  19669  plydivex  19679  plyexmo  19695  aannenlem1  19710  aaliou3lem2  19725  dvntaylp  19752  taylthlem1  19754  ulmval  19761  cxpmul2  20038  scvxcvx  20282  jensenlem2  20284  jensen  20285  ppiub  20445  bcmono  20518  bpos1lem  20523  bposlem5  20529  lgsquad2lem2  20600  dchrisumlem1  20640  dchrisum0flb  20661  pntpbnd1  20737  pntlemf  20756  qabvle  20776  qabvexp  20777  ostthlem2  20779  ostth2lem2  20785  elghomlem2  21031  isrngo  21047  rngodm1dm2  21087  hlim2  21773  elnlfn  22510  stle0i  22821  hstrbi  22848  spansncv2  22875  h1da  22931  ballotlem2  23049  xreceu  23107  fmptcof2  23231  tpr2rico  23298  hasheuni  23455  ismeas  23532  dstfrvunirn  23677  subfacp1lem6  23718  cvmliftlem7  23824  cvmliftlem10  23827  cvmlift2lem12  23847  cvmlift3lem4  23855  iseupa  23883  eupath2  23906  ghomf1olem  24003  climuzcnv  24006  relexpsucr  24028  relexpsucl  24030  relexpcnv  24031  relexprel  24033  relexpdm  24034  relexprn  24035  relexpfld  24036  relexpadd  24037  relexpindlem  24038  rtrclreclem.trans  24045  rtrclreclem.min  24046  rtrclind  24048  dedekindle  24085  fprb  24131  dfon2lem9  24149  trpredtr  24235  trpredmintr  24236  dftrpred3g  24238  trpredrec  24243  soseq  24256  wfrlem12  24269  frrlem11  24295  sltval2  24312  sltsolem1  24324  axeuclidlem  24592  axcontlem12  24605  linethru  24778  elhf2  24807  hfext  24815  nndivsub  24898  phthps  25007  elo  25052  imgfldref2  25075  f1ofi  25081  fixpb  25104  celsor  25122  injrec2  25130  surjsec2  25131  mapmapmap  25159  jidd  25203  midd  25204  int2pre  25248  defse3  25283  toplat  25301  rzrlzreq  25347  trran2  25404  ltrran2  25414  ltrooo  25415  rngodmeqrn  25430  rngoridfz  25448  truni1  25516  intopcoaconlem3b  25549  intopcoaconlem3  25550  fisub  25565  flfnei2  25588  islimrs3  25592  islimrs4  25593  trran  25625  trnij  25626  lvsovso  25637  cnegvex2  25671  rnegvex2  25672  addcanrg  25678  negveud  25679  negveudr  25680  clsmulcv  25693  fnmulcv  25695  distmlva  25699  hdrmp  25717  imonclem  25824  isepic  25835  tartarmap  25899  partarelt2  25908  carinttar  25913  grphidmor2  25964  cmpmor  25986  lemindclsbu  26006  pgapspf2  26064  gltpntl  26083  xsyysx  26156  nbssntrs  26158  isibcg  26202  finminlem  26242  fnessref  26304  lfinpfin  26314  locfincmp  26315  comppfsc  26318  neibastop2lem  26320  fnemeet2  26327  cover2  26369  upixp  26414  sdclem2  26463  fdc  26466  seqpo  26468  metf1o  26480  mettrifi  26484  sstotbnd3  26511  heibor1lem  26544  heiborlem5  26550  heibor  26556  bfplem1  26557  grpokerinj  26586  ispridl2  26674  mzpsubst  26837  jm2.18  27092  wepwsolem  27149  pm14.24  27643  stoweidlem2  27762  stoweidlem17  27777  stoweidlem21  27781  2reu2  27976  funbrafv  28031  ndmaovass  28077  elprchashprn2  28099  usgraedgprv  28133  usgranloop  28135  cusgra2v  28169  cusgrauvtx  28179  frgra2v  28188  frgra3vlem1  28189  3vfriswmgra  28194  1to2vfriswmgra  28195  1to3vfriswmgra  28196  sbcoreleleqVD  28708  csbxpgVD  28743  bnj607  29021  bnj1145  29096  bnj1204  29115  ax10lem17ALT  29196  ax9lem17  29229  lssatle  29278  4atexlemex4  30335
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 177  df-an 360
  Copyright terms: Public domain W3C validator