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  1879  cbval2  1944  cbvex2  1945  2moswap  2218  2mos  2222  2eu2  2224  pm2.61ne  2521  r19.21be  2644  uneqdifeq  3542  ssunsn2  3773  ssuni  3849  uniss2  3858  elpwuni  3989  elssabg  4166  elpw2g  4174  oteqex  4259  epelg  4306  wereu  4389  ordtr2  4436  ordsssuc2  4481  difex2  4525  ordpwsuc  4606  ordsucun  4616  limuni3  4643  ordom  4665  relop  4834  riinint  4935  sotri3  5073  unixpid  5207  cnviin  5212  funopg  5286  fun  5405  tz6.12c  5547  fvmptnf  5617  fmptco  5691  fnressn  5705  fressnfv  5707  fconst2g  5728  isores3  5832  isoselem  5838  eloprabga  5934  fo1stres  6143  poxp  6227  soxp  6228  brtpos2  6240  sorpsscmpl  6288  onnseq  6361  smores  6369  smofvon2  6373  oacl  6534  omcl  6535  oecl  6536  oawordri  6548  oalimcl  6558  oaass  6559  oarec  6560  omwordri  6570  omeulem1  6580  omeulem2  6581  oeordi  6585  oeworde  6591  oeoelem  6596  nnacl  6609  nnmcl  6610  nnecl  6611  nnacom  6615  nnaass  6620  nnmsucr  6623  nnmordi  6629  omabs  6645  iiner  6731  th3qlem2  6765  elpmg  6786  pmss12g  6794  mapsn  6809  f1domg  6881  ssdomg  6907  domtriord  7007  php  7045  php3  7047  1sdom  7065  fisseneq  7074  isinf  7076  ssnnfi  7082  dif1enOLD  7090  dif1en  7091  findcard3  7100  frfi  7102  unfi  7124  difinf  7127  fnfi  7134  iunfi  7144  elfi2  7168  marypha1lem  7186  marypha1  7187  oiexg  7250  harword  7279  brwdom  7281  unxpwdom  7303  inf3lemd  7328  inf3lem5  7333  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cnfcom  7403  en3lplem1  7416  tcmin  7426  r1sdom  7446  rankxplim3  7551  cardidm  7592  cardmin2  7631  infxpenlem  7641  fseqenlem1  7651  numacn  7676  alephordi  7701  iscard3  7720  alephinit  7722  carduniima  7723  iunfictbso  7741  dfac5  7755  dfac12lem3  7771  pwsdompw  7830  pwcdadom  7842  cflim2  7889  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  alephsing  7902  infpssALT  7939  fin23lem34  7972  isf32lem2  7980  isf32lem10  7988  isf32lem12  7990  isfin1-2  8011  hsmexlem4  8055  axcc2lem  8062  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ac6num  8106  ac6s  8111  zorn2lem7  8129  ttukeylem5  8140  imadomg  8159  iundom2g  8162  ondomon  8185  ficard  8187  konigthlem  8190  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  axregndlem1  8224  axregnd  8226  pwfseqlem3  8282  pwxpndom2  8287  pwxpndom  8288  pwcdandom  8289  inawinalem  8311  gchina  8321  wuncval2  8369  tsk0  8385  tskxpss  8394  inatsk  8400  tskuni  8405  gruina  8440  grothac  8452  addclpi  8516  addnidpi  8525  nqereu  8553  mulcanenq  8584  genpnnp  8629  nqpr  8638  prlem934  8657  reclem2pr  8672  suplem1pr  8676  mulcmpblnr  8696  supsrlem  8733  axpre-sup  8791  1re  8837  00id  8987  receu  9413  sup3  9711  peano5nni  9749  nnaddcl  9768  zrevaddcl  10063  zdiv  10082  nneo  10095  zeo2  10098  fzind  10110  fnn0ind  10111  uzwo  10281  uzwoOLD  10282  lbzbi  10306  qrevaddcl  10338  irradd  10340  irrmul  10341  ltsubrp  10385  ltaddrp  10386  icoshft  10758  fzen  10811  elfzm11  10853  uzsplit  10855  om2uzlti  11013  seqcl2  11064  seqfveq2  11068  seqshft2  11072  monoord  11076  seqsplit  11079  seqcaopr3  11081  seqf1olem2a  11084  seqf1o  11087  seqid2  11092  seqhomo  11093  ser1const  11102  expadd  11144  expmul  11147  leexp1a  11160  faccl  11298  facdiv  11300  faclbnd  11303  faclbnd4lem4  11309  faclbnd6  11312  hashgadd  11359  hashdomi  11362  hashunsng  11367  hashmap  11387  hashf1lem2  11394  hashf1  11395  seqcoll  11401  sswrd  11423  shftlem  11563  caubnd  11842  rlimcld2  12052  o1dif  12103  climub  12135  climserle  12136  iseraltlem2  12155  sumss  12197  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  cvgrat  12339  sin01gt0  12470  ruclem8  12515  ruclem9  12516  dvds2ln  12559  dvdslelem  12573  alzdvds  12578  ndvdsadd  12607  bitsinv1  12633  sadcadd  12649  sadadd2  12651  saddisjlem  12655  smuval2  12673  smupvallem  12674  smu01lem  12676  smupval  12679  smueqlem  12681  smumullem  12683  gcddiv  12728  gcdmultiple  12729  rplpwr  12735  nn0seqcvgd  12740  seq1st  12741  alginv  12745  algcvga  12749  algfx  12750  isprm2  12766  isprm3  12767  prmind2  12769  maxprmfct  12792  prmdvdsexp  12793  pcmpt  12940  prmreclem4  12966  vdwmc2  13026  vdwlem10  13037  ramub2  13061  ramcl  13076  imasleval  13443  divsfval  13449  mreexexlem4d  13549  isssc  13697  istos  14141  frmdgsum  14484  mhmmulg  14599  resghm2b  14701  elsymgbas  14774  gsumwrev  14839  odlem1  14850  odcl2  14878  gexlem1  14890  sylow1lem1  14909  efgi2  15034  efginvrel2  15036  efgsrel  15043  cyggexb  15185  gsummulglem  15213  gsum2d  15223  dmdprd  15236  dprdw  15245  ablfac1eulem  15307  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  cnfldmulg  16406  cnfldexp  16407  obslbs  16630  fctop  16741  mretopd  16829  restopnb  16906  restdis  16909  tgcnp  16983  cncls2  17002  cncls  17003  cnntr  17004  cnsscnp  17008  cmpsub  17127  2ndcsep  17185  1stcelcls  17187  txcn  17320  txlm  17342  xkohaus  17347  qtopres  17389  haushmphlem  17478  cmphmph  17479  conhmph  17480  reghmph  17484  nrmhmph  17485  ptcmpfi  17504  reghaus  17516  fbssfi  17532  fbun  17535  fbfinnfr  17536  isfildlem  17552  fgcl  17573  cfinfil  17588  supfil  17590  ufinffr  17624  fin1aufil  17627  cnpflf  17696  alexsubALTlem3  17743  alexsubALT  17745  tmdmulg  17775  tmdgsum  17778  tgphaus  17799  tgpt1  17800  mettri  17916  imasdsf1olem  17937  blssex  17973  mopni3  18040  metss  18054  dscmet  18095  rectbntr0  18337  metnrmlem1a  18362  fsumcn  18374  lmmbr  18684  caubl  18733  caublcls  18734  bcthlem5  18750  bcth3  18753  ovolunlem1a  18855  ovoliunnul  18866  ovolicc2lem3  18878  finiunmbl  18901  voliunlem1  18907  volsuplem  18912  volsup  18913  dyadmax  18953  itgfsum  19181  dvnadd  19278  dvnres  19280  cpnord  19284  dvnfre  19301  dvmptfsum  19322  dvlip  19340  pf1ind  19438  fta1g  19553  plyco  19623  dgrcolem1  19654  dgrco  19656  dvnply2  19667  plydivex  19677  plyexmo  19693  aannenlem1  19708  aaliou3lem2  19723  dvntaylp  19750  taylthlem1  19752  ulmval  19759  cxpmul2  20036  scvxcvx  20280  jensenlem2  20282  jensen  20283  ppiub  20443  bcmono  20516  bpos1lem  20521  bposlem5  20527  lgsquad2lem2  20598  dchrisumlem1  20638  dchrisum0flb  20659  pntpbnd1  20735  pntlemf  20754  qabvle  20774  qabvexp  20775  ostthlem2  20777  ostth2lem2  20783  elghomlem2  21029  isrngo  21045  rngodm1dm2  21085  hlim2  21771  elnlfn  22508  stle0i  22819  hstrbi  22846  spansncv2  22873  h1da  22929  ballotlem2  23047  xreceu  23105  fmptcof2  23229  tpr2rico  23296  hasheuni  23453  ismeas  23530  dstfrvunirn  23675  subfacp1lem6  23716  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift2lem12  23845  cvmlift3lem4  23853  iseupa  23881  eupath2  23904  ghomf1olem  24001  climuzcnv  24004  relexpsucr  24026  relexpsucl  24028  relexpcnv  24029  relexprel  24031  relexpdm  24032  relexprn  24033  relexpfld  24034  relexpadd  24035  relexpindlem  24036  rtrclreclem.trans  24043  rtrclreclem.min  24044  rtrclind  24046  dedekindle  24083  fprb  24129  dfon2lem9  24147  trpredtr  24233  trpredmintr  24234  dftrpred3g  24236  trpredrec  24241  soseq  24254  wfrlem12  24267  frrlem11  24293  sltval2  24310  sltsolem1  24322  axeuclidlem  24590  axcontlem12  24603  linethru  24776  elhf2  24805  hfext  24813  nndivsub  24896  phthps  24996  elo  25041  imgfldref2  25064  f1ofi  25070  fixpb  25093  celsor  25111  injrec2  25119  surjsec2  25120  mapmapmap  25148  jidd  25192  midd  25193  int2pre  25237  defse3  25272  toplat  25290  rzrlzreq  25336  trran2  25393  ltrran2  25403  ltrooo  25404  rngodmeqrn  25419  rngoridfz  25437  truni1  25505  intopcoaconlem3b  25538  intopcoaconlem3  25539  fisub  25554  flfnei2  25577  islimrs3  25581  islimrs4  25582  trran  25614  trnij  25615  lvsovso  25626  cnegvex2  25660  rnegvex2  25661  addcanrg  25667  negveud  25668  negveudr  25669  clsmulcv  25682  fnmulcv  25684  distmlva  25688  hdrmp  25706  imonclem  25813  isepic  25824  tartarmap  25888  partarelt2  25897  carinttar  25902  grphidmor2  25953  cmpmor  25975  lemindclsbu  25995  pgapspf2  26053  gltpntl  26072  xsyysx  26145  nbssntrs  26147  isibcg  26191  finminlem  26231  fnessref  26293  lfinpfin  26303  locfincmp  26304  comppfsc  26307  neibastop2lem  26309  fnemeet2  26316  cover2  26358  upixp  26403  sdclem2  26452  fdc  26455  seqpo  26457  metf1o  26469  mettrifi  26473  sstotbnd3  26500  heibor1lem  26533  heiborlem5  26539  heibor  26545  bfplem1  26546  grpokerinj  26575  ispridl2  26663  mzpsubst  26826  jm2.18  27081  wepwsolem  27138  pm14.24  27632  stoweidlem2  27751  stoweidlem17  27766  stoweidlem21  27770  2reu2  27965  funbrafv  28020  ndmaovass  28066  elprchashprn2  28088  usgraedgprv  28122  usgranloop  28124  cusgra2v  28158  cusgrauvtx  28168  frgra2v  28177  frgra3vlem1  28178  3vfriswmgra  28183  1to2vfriswmgra  28184  1to3vfriswmgra  28185  sbcoreleleqVD  28635  csbxpgVD  28670  bnj607  28948  bnj1145  29023  bnj1204  29042  ax10lem17ALT  29123  ax9lem17  29156  lssatle  29205  4atexlemex4  30262
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