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  1892  cbval2  1957  cbvex2  1958  2moswap  2231  2mos  2235  2eu2  2237  pm2.61ne  2534  r19.21be  2657  uneqdifeq  3555  ssunsn2  3789  ssuni  3865  uniss2  3874  elpwuni  4005  elssabg  4182  elpw2g  4190  oteqex  4275  epelg  4322  wereu  4405  ordtr2  4452  ordsssuc2  4497  difex2  4541  ordpwsuc  4622  ordsucun  4632  limuni3  4659  ordom  4681  relop  4850  riinint  4951  sotri3  5089  unixpid  5223  cnviin  5228  funopg  5302  fun  5421  tz6.12c  5563  fvmptnf  5633  fmptco  5707  fnressn  5721  fressnfv  5723  fconst2g  5744  isores3  5848  isoselem  5854  eloprabga  5950  fo1stres  6159  poxp  6243  soxp  6244  brtpos2  6256  sorpsscmpl  6304  onnseq  6377  smores  6385  smofvon2  6389  oacl  6550  omcl  6551  oecl  6552  oawordri  6564  oalimcl  6574  oaass  6575  oarec  6576  omwordri  6586  omeulem1  6596  omeulem2  6597  oeordi  6601  oeworde  6607  oeoelem  6612  nnacl  6625  nnmcl  6626  nnecl  6627  nnacom  6631  nnaass  6636  nnmsucr  6639  nnmordi  6645  omabs  6661  iiner  6747  th3qlem2  6781  elpmg  6802  pmss12g  6810  mapsn  6825  f1domg  6897  ssdomg  6923  domtriord  7023  php  7061  php3  7063  1sdom  7081  fisseneq  7090  isinf  7092  ssnnfi  7098  dif1enOLD  7106  dif1en  7107  findcard3  7116  frfi  7118  unfi  7140  difinf  7143  fnfi  7150  iunfi  7160  elfi2  7184  marypha1lem  7202  marypha1  7203  oiexg  7266  harword  7295  brwdom  7297  unxpwdom  7319  inf3lemd  7344  inf3lem5  7349  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cnfcom  7419  en3lplem1  7432  tcmin  7442  r1sdom  7462  rankxplim3  7567  cardidm  7608  cardmin2  7647  infxpenlem  7657  fseqenlem1  7667  numacn  7692  alephordi  7717  iscard3  7736  alephinit  7738  carduniima  7739  iunfictbso  7757  dfac5  7771  dfac12lem3  7787  pwsdompw  7846  pwcdadom  7858  cflim2  7905  cfslb2n  7910  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  alephsing  7918  infpssALT  7955  fin23lem34  7988  isf32lem2  7996  isf32lem10  8004  isf32lem12  8006  isfin1-2  8027  hsmexlem4  8071  axcc2lem  8078  domtriomlem  8084  axdc2lem  8090  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  ac6num  8122  ac6s  8127  zorn2lem7  8145  ttukeylem5  8156  imadomg  8175  iundom2g  8178  ondomon  8201  ficard  8203  konigthlem  8206  alephreg  8220  pwcfsdom  8221  cfpwsdom  8222  axregndlem1  8240  axregnd  8242  pwfseqlem3  8298  pwxpndom2  8303  pwxpndom  8304  pwcdandom  8305  inawinalem  8327  gchina  8337  wuncval2  8385  tsk0  8401  tskxpss  8410  inatsk  8416  tskuni  8421  gruina  8456  grothac  8468  addclpi  8532  addnidpi  8541  nqereu  8569  mulcanenq  8600  genpnnp  8645  nqpr  8654  prlem934  8673  reclem2pr  8688  suplem1pr  8692  mulcmpblnr  8712  supsrlem  8749  axpre-sup  8807  1re  8853  00id  9003  receu  9429  sup3  9727  peano5nni  9765  nnaddcl  9784  zrevaddcl  10079  zdiv  10098  nneo  10111  zeo2  10114  fzind  10126  fnn0ind  10127  uzwo  10297  uzwoOLD  10298  lbzbi  10322  qrevaddcl  10354  irradd  10356  irrmul  10357  ltsubrp  10401  ltaddrp  10402  icoshft  10774  fzen  10827  elfzm11  10869  uzsplit  10871  om2uzlti  11029  seqcl2  11080  seqfveq2  11084  seqshft2  11088  monoord  11092  seqsplit  11095  seqcaopr3  11097  seqf1olem2a  11100  seqf1o  11103  seqid2  11108  seqhomo  11109  ser1const  11118  expadd  11160  expmul  11163  leexp1a  11176  faccl  11314  facdiv  11316  faclbnd  11319  faclbnd4lem4  11325  faclbnd6  11328  hashgadd  11375  hashdomi  11378  hashunsng  11383  hashmap  11403  hashf1lem2  11410  hashf1  11411  seqcoll  11417  sswrd  11439  shftlem  11579  caubnd  11858  rlimcld2  12068  o1dif  12119  climub  12151  climserle  12152  iseraltlem2  12171  sumss  12213  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  bcxmas  12310  climcndslem1  12324  climcndslem2  12325  cvgrat  12355  sin01gt0  12486  ruclem8  12531  ruclem9  12532  dvds2ln  12575  dvdslelem  12589  alzdvds  12594  ndvdsadd  12623  bitsinv1  12649  sadcadd  12665  sadadd2  12667  saddisjlem  12671  smuval2  12689  smupvallem  12690  smu01lem  12692  smupval  12695  smueqlem  12697  smumullem  12699  gcddiv  12744  gcdmultiple  12745  rplpwr  12751  nn0seqcvgd  12756  seq1st  12757  alginv  12761  algcvga  12765  algfx  12766  isprm2  12782  isprm3  12783  prmind2  12785  maxprmfct  12808  prmdvdsexp  12809  pcmpt  12956  prmreclem4  12982  vdwmc2  13042  vdwlem10  13053  ramub2  13077  ramcl  13092  imasleval  13459  divsfval  13465  mreexexlem4d  13565  isssc  13713  istos  14157  frmdgsum  14500  mhmmulg  14615  resghm2b  14717  elsymgbas  14790  gsumwrev  14855  odlem1  14866  odcl2  14894  gexlem1  14906  sylow1lem1  14925  efgi2  15050  efginvrel2  15052  efgsrel  15059  cyggexb  15201  gsummulglem  15229  gsum2d  15239  dmdprd  15252  dprdw  15261  ablfac1eulem  15323  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  cnfldmulg  16422  cnfldexp  16423  obslbs  16646  fctop  16757  mretopd  16845  restopnb  16922  restdis  16925  tgcnp  16999  cncls2  17018  cncls  17019  cnntr  17020  cnsscnp  17024  cmpsub  17143  2ndcsep  17201  1stcelcls  17203  txcn  17336  txlm  17358  xkohaus  17363  qtopres  17405  haushmphlem  17494  cmphmph  17495  conhmph  17496  reghmph  17500  nrmhmph  17501  ptcmpfi  17520  reghaus  17532  fbssfi  17548  fbun  17551  fbfinnfr  17552  isfildlem  17568  fgcl  17589  cfinfil  17604  supfil  17606  ufinffr  17640  fin1aufil  17643  cnpflf  17712  alexsubALTlem3  17759  alexsubALT  17761  tmdmulg  17791  tmdgsum  17794  tgphaus  17815  tgpt1  17816  mettri  17932  imasdsf1olem  17953  blssex  17989  mopni3  18056  metss  18070  dscmet  18111  rectbntr0  18353  metnrmlem1a  18378  fsumcn  18390  lmmbr  18700  caubl  18749  caublcls  18750  bcthlem5  18766  bcth3  18769  ovolunlem1a  18871  ovoliunnul  18882  ovolicc2lem3  18894  finiunmbl  18917  voliunlem1  18923  volsuplem  18928  volsup  18929  dyadmax  18969  itgfsum  19197  dvnadd  19294  dvnres  19296  cpnord  19300  dvnfre  19317  dvmptfsum  19338  dvlip  19356  pf1ind  19454  fta1g  19569  plyco  19639  dgrcolem1  19670  dgrco  19672  dvnply2  19683  plydivex  19693  plyexmo  19709  aannenlem1  19724  aaliou3lem2  19739  dvntaylp  19766  taylthlem1  19768  ulmval  19775  cxpmul2  20052  scvxcvx  20296  jensenlem2  20298  jensen  20299  ppiub  20459  bcmono  20532  bpos1lem  20537  bposlem5  20543  lgsquad2lem2  20614  dchrisumlem1  20654  dchrisum0flb  20675  pntpbnd1  20751  pntlemf  20770  qabvle  20790  qabvexp  20791  ostthlem2  20793  ostth2lem2  20799  elghomlem2  21045  isrngo  21061  rngodm1dm2  21101  hlim2  21787  elnlfn  22524  stle0i  22835  hstrbi  22862  spansncv2  22889  h1da  22945  ballotlem2  23063  xreceu  23121  fmptcof2  23244  tpr2rico  23311  hasheuni  23468  ismeas  23545  dstfrvunirn  23690  subfacp1lem6  23731  cvmliftlem7  23837  cvmliftlem10  23840  cvmlift2lem12  23860  cvmlift3lem4  23868  iseupa  23896  eupath2  23919  ghomf1olem  24016  climuzcnv  24019  relexpsucr  24041  relexpsucl  24043  relexpcnv  24044  relexprel  24046  relexpdm  24047  relexprn  24048  relexpfld  24049  relexpadd  24050  relexpindlem  24051  rtrclreclem.trans  24058  rtrclreclem.min  24059  rtrclind  24061  dedekindle  24098  fprb  24200  dfon2lem9  24218  trpredtr  24304  trpredmintr  24305  dftrpred3g  24307  trpredrec  24312  soseq  24325  wfrlem12  24338  frrlem11  24364  sltval2  24381  sltsolem1  24393  axeuclidlem  24662  axcontlem12  24675  linethru  24848  elhf2  24877  hfext  24885  nndivsub  24968  ovoliunnfl  25001  phthps  25099  elo  25144  imgfldref2  25167  f1ofi  25173  fixpb  25196  celsor  25214  injrec2  25222  surjsec2  25223  mapmapmap  25251  jidd  25295  midd  25296  int2pre  25340  defse3  25375  toplat  25393  rzrlzreq  25439  trran2  25496  ltrran2  25506  ltrooo  25507  rngodmeqrn  25522  rngoridfz  25540  truni1  25608  intopcoaconlem3b  25641  intopcoaconlem3  25642  fisub  25657  flfnei2  25680  islimrs3  25684  islimrs4  25685  trran  25717  trnij  25718  lvsovso  25729  cnegvex2  25763  rnegvex2  25764  addcanrg  25770  negveud  25771  negveudr  25772  clsmulcv  25785  fnmulcv  25787  distmlva  25791  hdrmp  25809  imonclem  25916  isepic  25927  tartarmap  25991  partarelt2  26000  carinttar  26005  grphidmor2  26056  cmpmor  26078  lemindclsbu  26098  pgapspf2  26156  gltpntl  26175  xsyysx  26248  nbssntrs  26250  isibcg  26294  finminlem  26334  fnessref  26396  lfinpfin  26406  locfincmp  26407  comppfsc  26410  neibastop2lem  26412  fnemeet2  26419  cover2  26461  upixp  26506  sdclem2  26555  fdc  26558  seqpo  26560  metf1o  26572  mettrifi  26576  sstotbnd3  26603  heibor1lem  26636  heiborlem5  26642  heibor  26648  bfplem1  26649  grpokerinj  26678  ispridl2  26766  mzpsubst  26929  jm2.18  27184  wepwsolem  27241  pm14.24  27735  stoweidlem2  27854  stoweidlem17  27869  stoweidlem21  27873  2reu2  28068  afveu  28121  funbrafv  28126  ndmaovass  28174  injresinjlem  28214  injresinj  28215  elprchashprn2  28216  usgraedgprv  28256  usgranloop  28258  nb3graprlem2  28288  cusgra2v  28297  cusgrauvtx  28309  usgrnloop  28351  wlkdvspthlem  28365  wlkdvspth  28366  cyclnspth  28376  fargshiftf  28381  fargshiftf1  28382  eupatrl  28385  3v3e3cycl2  28410  3v3e3cycl  28411  4cycl4dv  28413  frgra2v  28423  frgra3vlem1  28424  3vfriswmgra  28429  1to2vfriswmgra  28430  1to3vfriswmgra  28431  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  4cycl2vnunb  28439  sbcoreleleqVD  28951  csbxpgVD  28986  bnj607  29264  bnj1145  29339  bnj1204  29358  dvelimvNEW7  29439  cbval2OLD7  29684  cbvex2OLD7  29685  ax10lem17ALT  29745  ax9lem17  29778  lssatle  29827  4atexlemex4  30884
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