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  1972  cbval2  2030  cbvex2  2031  2moswap  2306  2eu2  2312  pm2.61ne  2618  r19.21be  2743  uneqdifeq  3652  ssunsn2  3894  ssuni  3972  uniss2  3981  elpwuni  4112  elssabg  4289  elpw2g  4297  oteqex  4383  epelg  4429  wereu  4512  ordtr2  4559  ordsssuc2  4603  difex2  4647  ordpwsuc  4728  ordsucun  4738  limuni3  4765  ordom  4787  relop  4956  riinint  5059  sotri3  5197  unixpid  5337  cnviin  5342  funopg  5418  fun  5540  tz6.12c  5683  fvmptnf  5754  eldmrexrnb  5809  fmptco  5833  fnressn  5850  fressnfv  5852  fvtp2g  5875  fvtp3g  5876  fconst2g  5878  isores3  5987  isoselem  5993  eloprabga  6092  fo1stres  6302  poxp  6387  soxp  6388  brtpos2  6414  sorpsscmpl  6462  onnseq  6535  smores  6543  smofvon2  6547  oacl  6708  omcl  6709  oecl  6710  oawordri  6722  oalimcl  6732  oaass  6733  oarec  6734  omwordri  6744  omeulem1  6754  omeulem2  6755  oeordi  6759  oeworde  6765  oeoelem  6770  nnacl  6783  nnmcl  6784  nnecl  6785  nnacom  6789  nnaass  6794  nnmsucr  6797  nnmordi  6803  omabs  6819  iiner  6905  th3qlem2  6940  elpmg  6961  pmss12g  6969  mapsn  6984  f1domg  7056  ssdomg  7082  domtriord  7182  php  7220  php3  7222  1sdom  7240  fisseneq  7249  isinf  7251  ssnnfi  7257  dif1enOLD  7269  dif1en  7270  findcard3  7279  frfi  7281  unfi  7303  difinf  7306  fnfi  7313  iunfi  7323  elfi2  7347  marypha1lem  7366  marypha1  7367  oiexg  7430  harword  7459  brwdom  7461  unxpwdom  7483  inf3lemd  7508  inf3lem5  7513  cantnfval2  7550  cantnfle  7552  cantnflt  7553  cnfcom  7583  en3lplem1  7596  tcmin  7606  r1sdom  7626  rankxplim3  7731  cardidm  7772  cardmin2  7811  infxpenlem  7821  fseqenlem1  7831  numacn  7856  alephordi  7881  iscard3  7900  alephinit  7902  carduniima  7903  iunfictbso  7921  dfac5  7935  dfac12lem3  7951  pwsdompw  8010  pwcdadom  8022  cflim2  8069  cfslb2n  8074  cofsmo  8075  cfsmolem  8076  cfcoflem  8078  alephsing  8082  infpssALT  8119  fin23lem34  8152  isf32lem2  8160  isf32lem10  8168  isf32lem12  8170  isfin1-2  8191  hsmexlem4  8235  axcc2lem  8242  domtriomlem  8248  axdc2lem  8254  axdc3lem2  8257  axdc3lem4  8259  axdc4lem  8261  axcclem  8263  ac6num  8285  ac6s  8290  zorn2lem7  8308  ttukeylem5  8319  imadomg  8338  iundom2g  8341  ondomon  8364  ficard  8366  konigthlem  8369  alephreg  8383  pwcfsdom  8384  cfpwsdom  8385  axregndlem1  8403  axregnd  8405  pwfseqlem3  8461  pwxpndom2  8466  pwxpndom  8467  pwcdandom  8468  inawinalem  8490  gchina  8500  wuncval2  8548  tsk0  8564  tskxpss  8573  inatsk  8579  tskuni  8584  gruina  8619  grothac  8631  addclpi  8695  addnidpi  8704  nqereu  8732  mulcanenq  8763  genpnnp  8808  nqpr  8817  prlem934  8836  reclem2pr  8851  suplem1pr  8855  mulcmpblnr  8875  supsrlem  8912  axpre-sup  8970  1re  9016  00id  9166  receu  9592  sup3  9890  peano5nni  9928  nnaddcl  9947  zrevaddcl  10246  zdiv  10265  nneo  10278  zeo2  10281  fzind  10293  fnn0ind  10294  uzwo  10464  uzwoOLD  10465  lbzbi  10489  qrevaddcl  10521  irradd  10523  irrmul  10524  ltsubrp  10568  ltaddrp  10569  icoshft  10944  fzen  10997  elfzm11  11039  uzsplit  11041  injresinjlem  11119  injresinj  11120  om2uzlti  11210  seqcl2  11261  seqfveq2  11265  seqshft2  11269  monoord  11273  seqsplit  11276  seqcaopr3  11278  seqf1olem2a  11281  seqf1o  11284  seqid2  11289  seqhomo  11290  ser1const  11299  expadd  11342  expmul  11345  leexp1a  11358  faccl  11496  facdiv  11498  faclbnd  11501  faclbnd4lem4  11507  faclbnd6  11510  hasheqf1oi  11555  hashgadd  11571  hashdomi  11574  hashinfxadd  11579  hashunx  11580  hashunsng  11585  elprchashprn2  11587  hashle00  11589  hash1snb  11601  hashmap  11618  hashf1lem2  11625  hashf1  11626  seqcoll  11632  brfi1uzind  11635  sswrd  11657  shftlem  11803  caubnd  12082  rlimcld2  12292  o1dif  12343  climub  12375  climserle  12376  iseraltlem2  12396  sumss  12438  fsum2d  12475  fsumabs  12500  fsumrlim  12510  fsumo1  12511  fsumiun  12520  bcxmas  12535  climcndslem1  12549  climcndslem2  12550  cvgrat  12580  sin01gt0  12711  ruclem8  12756  ruclem9  12757  dvds2ln  12800  dvdslelem  12814  alzdvds  12819  ndvdsadd  12848  bitsinv1  12874  sadcadd  12890  sadadd2  12892  saddisjlem  12896  smuval2  12914  smupvallem  12915  smu01lem  12917  smupval  12920  smueqlem  12922  smumullem  12924  gcddiv  12969  gcdmultiple  12970  rplpwr  12976  nn0seqcvgd  12981  seq1st  12982  alginv  12986  algcvga  12990  algfx  12991  isprm2  13007  isprm3  13008  prmind2  13010  maxprmfct  13033  prmdvdsexp  13034  pcmpt  13181  prmreclem4  13207  vdwmc2  13267  vdwlem10  13278  ramub2  13302  ramcl  13317  imasleval  13686  divsfval  13692  mreexexlem4d  13792  isssc  13940  istos  14384  frmdgsum  14727  mhmmulg  14842  resghm2b  14944  elsymgbas  15017  gsumwrev  15082  odlem1  15093  odcl2  15121  gexlem1  15133  sylow1lem1  15152  efgi2  15277  efginvrel2  15279  efgsrel  15286  cyggexb  15428  gsummulglem  15456  gsum2d  15466  dmdprd  15479  dprdw  15488  ablfac1eulem  15550  mplcoe1  16448  mplcoe3  16449  mplcoe2  16450  cnfldmulg  16649  cnfldexp  16650  obslbs  16873  fctop  16984  mretopd  17072  restopnb  17154  restdis  17157  tgcnp  17232  cncls2  17252  cncls  17253  cnntr  17254  cnsscnp  17258  cmpsub  17378  2ndcsep  17436  1stcelcls  17438  txcn  17572  txlm  17594  xkohaus  17599  qtopres  17644  haushmphlem  17733  cmphmph  17734  conhmph  17735  reghmph  17739  nrmhmph  17740  ptcmpfi  17759  reghaus  17771  fbssfi  17783  fbun  17786  fbfinnfr  17787  isfildlem  17803  fgcl  17824  cfinfil  17839  supfil  17841  ufinffr  17875  fin1aufil  17878  cnpflf  17947  alexsubALTlem3  17994  alexsubALT  17996  cnextfvval  18010  cnextcn  18012  tmdmulg  18036  tmdgsum  18039  tgphaus  18060  tgpt1  18061  mettri  18283  imasdsf1olem  18304  blssex  18340  mopni3  18407  metss  18421  metutop  18480  dscmet  18484  rectbntr0  18727  metnrmlem1a  18752  fsumcn  18764  lmmbr  19075  caubl  19124  caublcls  19125  bcthlem5  19143  bcth3  19146  ovolunlem1a  19252  ovoliunnul  19263  ovolicc2lem3  19275  finiunmbl  19298  voliunlem1  19304  volsuplem  19309  volsup  19310  dyadmax  19350  itgfsum  19578  dvnadd  19675  dvnres  19677  cpnord  19681  dvnfre  19698  dvmptfsum  19719  dvlip  19737  pf1ind  19835  fta1g  19950  plyco  20020  dgrcolem1  20051  dgrco  20053  dvnply2  20064  plydivex  20074  plyexmo  20090  aannenlem1  20105  aaliou3lem2  20120  dvntaylp  20147  taylthlem1  20149  ulmval  20156  cxpmul2  20440  scvxcvx  20684  jensenlem2  20686  jensen  20687  ppiub  20848  bcmono  20921  bpos1lem  20926  bposlem5  20932  lgsquad2lem2  21003  dchrisumlem1  21043  dchrisum0flb  21064  pntpbnd1  21140  pntlemf  21159  qabvle  21179  qabvexp  21180  ostthlem2  21182  ostth2lem2  21188  usgraedgprv  21256  usgraidx2vlem2  21270  usgrafisbase  21287  edgusgranbfin  21318  nb3graprlem2  21320  cusgra2v  21330  cusgrafi  21350  sizeusglecusglem1  21352  sizeusglecusg  21354  usgramaxsize  21355  usgrnloop  21412  constr2trl  21439  wlkdvspthlem  21448  wlkdvspth  21449  cyclnspth  21459  fargshiftf  21464  fargshiftf1  21465  3v3e3cycl2  21492  3v3e3cycl  21493  4cycl4dv  21495  iseupa  21528  eupatrl  21531  eupath2  21543  elghomlem2  21791  isrngo  21807  rngodm1dm2  21847  rngoridfz  21864  hlim2  22535  elnlfn  23272  stle0i  23583  hstrbi  23610  spansncv2  23637  h1da  23693  fmptcof2  23911  xreceu  23999  tpr2rico  24107  hasheuni  24264  ismeas  24342  rrvsum  24484  dstfrvunirn  24504  subfacp1lem6  24643  cvmliftlem7  24750  cvmliftlem10  24753  cvmlift2lem12  24773  cvmlift3lem4  24781  ghomf1olem  24877  climuzcnv  24880  relexpsucr  24902  relexpsucl  24904  relexpcnv  24905  relexprel  24906  relexpdm  24907  relexprn  24908  relexpfld  24909  relexpadd  24910  relexpindlem  24911  rtrclreclem.trans  24918  rtrclreclem.min  24919  rtrclind  24921  dedekindle  24960  clim2prod  24988  prodfn0  24994  prodfrec  24995  ntrivcvg  24997  prodmo  25034  fprodss  25046  fprodabs  25069  fprodefsum  25070  fprodn0  25075  fprb  25146  dfon2lem9  25164  trpredtr  25250  trpredmintr  25251  dftrpred3g  25253  trpredrec  25258  soseq  25271  wfrlem12  25284  frrlem11  25310  sltval2  25327  sltsolem1  25339  axeuclidlem  25608  axcontlem12  25621  linethru  25794  elhf2  25823  hfext  25831  nndivsub  25914  ovoliunnfl  25946  voliunnfl  25948  volsupnfl  25949  finminlem  26005  fnessref  26057  lfinpfin  26067  locfincmp  26068  comppfsc  26071  neibastop2lem  26073  fnemeet2  26080  cover2  26099  upixp  26115  sdclem2  26130  fdc  26133  seqpo  26135  metf1o  26145  mettrifi  26147  sstotbnd3  26169  heibor1lem  26202  heiborlem5  26208  heibor  26214  bfplem1  26215  grpokerinj  26244  ispridl2  26332  mzpsubst  26489  jm2.18  26743  wepwsolem  26800  stoweidlem2  27412  stoweidlem17  27427  stoweidlem21  27431  2reu2  27626  afveu  27679  funbrafv  27684  ndmaovass  27732  frgra2v  27745  frgra3vlem1  27746  3vfriswmgra  27751  1to2vfriswmgra  27752  1to3vfriswmgra  27753  2pthfrgra  27757  3cyclfrgrarn1  27758  3cyclfrgrarn  27759  3cyclfrgrarn2  27760  4cycl2vnunb  27763  vdn0frgrav2  27770  vdgn0frgrav2  27771  frgrancvvdeqlem4  27778  frgrancvvdeqlemB  27783  frgrancvvdeqlemC  27784  frgrawopreglem2  27790  frgrawopreglem4  27792  frgrawopreg  27794  frgraregorufr0  27797  sbcoreleleqVD  28305  csbxpgVD  28340  bnj607  28618  bnj1145  28693  bnj1204  28712  dvelimvNEW7  28793  cbval2OLD7  29039  cbvex2OLD7  29040  ax10lem17ALT  29099  ax9lem17  29132  lssatle  29181  4atexlemex4  30238
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