Theorem expcom 116

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

Step	Hyp	Ref	Expression
1		exp.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 115	. 2 |- ( ph -> ( ps -> ch ) )
3	2	com12 30	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  559  pm4.79dc  905  dedlema  972  dedlemb  973  19.35-1  1648  cbval2  1946  cbvex2  1947  nelelne  2470  r19.21be  2599  r19.35-1  2658  mosubt  2957  sbcrext  3083  uneqdifeqim  3554  ssuni  3886  uniss2  3895  elpwuni  4031  elssabg  4208  elpw2g  4216  epelg  4355  elomssom  4671  relop  4846  riinint  4958  cnviinm  5243  funopg  5324  fun  5469  tz6.12c  5629  fvelrnb  5649  fmptco  5769  funopsn  5785  fnressn  5793  fressnfv  5794  fvtp2g  5816  fvtp3g  5817  fconst2g  5822  isores3  5907  isoselem  5912  eloprabga  6055  fo1stresm  6270  poxp  6341  brtpos2  6360  smores  6401  tfrlem1  6417  tfrlemi1  6441  tfr1onlemaccex  6457  tfrcllemaccex  6470  frecrdg  6517  oawordriexmid  6579  nnacl  6589  nnmcl  6590  nnacom  6593  nnaass  6594  nnmsucr  6597  nndifsnid  6616  nnmordi  6625  iinerm  6717  th3qlem2  6748  elpmg  6774  pmss12g  6785  mapsn  6800  brdomg  6860  f1domg  6872  ssdomg  6893  nndomo  6986  elfi2  7100  nnnninfeq2  7257  carden2bex  7323  cc3  7415  addclpi  7475  addnidpig  7484  genpassl  7672  genpassu  7673  nqprloc  7693  ltaprlem  7766  recexprlemopl  7773  recexprlemopu  7775  recexprlemupu  7776  recexprlemss1l  7783  recexprlemss1u  7784  cauappcvgprlemupu  7797  caucvgprlemupu  7820  caucvgprprlemupu  7848  archsr  7930  peano2nnnn  8001  receuap  8777  peano2nn  9083  nnaddcl  9091  zrevaddcl  9458  nzadd  9460  zdiv  9496  nneo  9511  zeo2  9514  peano5uzti  9516  fzind  9523  fnn0ind  9524  lbzbi  9772  qrevaddcl  9800  irradd  9802  irrmul  9803  ltsubrp  9847  ltaddrp  9848  xnn0xadd0  10024  icoshft  10147  fzen  10200  elfzm11  10248  uzsplit  10249  fzoval  10305  elfzom1elp1fzo  10368  exfzdc  10406  modaddmodup  10569  frec2uzrdg  10591  nninfinf  10625  seq3clss  10653  monoord  10667  seq3caopr3  10673  seqcaopr3g  10674  seq3f1olemp  10697  seqf1oglem2a  10700  seqf1og  10703  seq3id3  10706  seq3homo  10709  seq3z  10710  seqfeq4g  10713  ser3ge0  10718  expadd  10763  expmul  10766  leexp1a  10776  modqexp  10848  faccl  10917  facdiv  10920  faclbnd  10923  faclbnd6  10926  omgadd  10984  hashunsng  10989  seq3coll  11024  fundm2domnop0  11027  swrdswrdlem  11195  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccat3  11225  shftlem  11242  resqrexlemover  11436  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc3  11442  climub  11770  climserle  11771  fsumzcl2  11831  fsumsplitsnun  11845  fsum2d  11861  modfsummodlemstep  11883  fsumabs  11891  fsumiun  11903  bcxmas  11915  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  prodfap0  11971  prodfrecap  11972  ntrivcvgap  11974  prodmodc  12004  fprodssdc  12016  fprodabs  12042  fprod2d  12049  dvdsmod0  12219  dvds2ln  12250  dvdsabseq  12273  dvdsdivcl  12276  alzdvds  12280  oddnn02np1  12306  m1exp1  12327  nn0o1gt2  12331  nno  12332  ndvdsadd  12357  flodddiv4  12362  bitsinv1  12388  gcddiv  12455  gcdmultiple  12456  gcdmultiplez  12457  rplpwr  12463  dvdssq  12467  nninfct  12477  nn0seqcvgd  12478  alginv  12484  algcvga  12488  algfx  12489  isprm2  12554  isprm3  12555  prmdvdsexp  12585  eulerthlemrprm  12666  eulerthlema  12667  pcmpt  12781  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemhom  12901  omiunct  12930  nninfdclemlt  12937  setsn0fun  12984  mgmcl  13306  dfgrp3mlem  13545  mhmmulg  13614  resghm2b  13713  gsumfzconst  13792  srgpcomp  13867  lmodfopnelem1  14201  rmodislmodlem  14227  lss1d  14260  cnfldmulg  14453  cnfldexp  14454  gsumfzfsumlemm  14464  restopnb  14768  restdis  14771  tgcnp  14796  cnntr  14812  cnsscnp  14816  txcn  14862  txlm  14866  mettri  14960  blssexps  15016  blssex  15017  mopni3  15071  metss  15081  dvmptfsum  15312  plycolemc  15345  rpcxpmul2  15500  gausslemma2dlem6  15659  lgsquad2lem2  15674  2lgslem1c  15682  2lgslem3  15693  2lgs  15696  uhgredgrnv  15844  2spim  15902