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  908  dedlema  975  dedlemb  976  19.35-1  1670  cbval2  1968  cbvex2  1969  nelelne  2492  r19.21be  2621  r19.35-1  2681  mosubt  2980  sbcrext  3106  uneqdifeqim  3577  ssuni  3909  uniss2  3918  elpwuni  4054  elssabg  4231  elpw2g  4239  epelg  4380  elomssom  4696  relop  4871  riinint  4984  cnviinm  5269  funopg  5351  fun  5496  tz6.12c  5656  fvelrnb  5680  fmptco  5800  funopsn  5816  fnressn  5824  fressnfv  5825  fvtp2g  5847  fvtp3g  5848  fconst2g  5853  isores3  5938  isoselem  5943  eloprabga  6090  fo1stresm  6305  poxp  6376  brtpos2  6395  smores  6436  tfrlem1  6452  tfrlemi1  6476  tfr1onlemaccex  6492  tfrcllemaccex  6505  frecrdg  6552  oawordriexmid  6614  nnacl  6624  nnmcl  6625  nnacom  6628  nnaass  6629  nnmsucr  6632  nndifsnid  6651  nnmordi  6660  iinerm  6752  th3qlem2  6783  elpmg  6809  pmss12g  6820  mapsn  6835  brdomg  6895  f1domg  6907  ssdomg  6928  nndomo  7021  elfi2  7135  nnnninfeq2  7292  carden2bex  7358  cc3  7450  addclpi  7510  addnidpig  7519  genpassl  7707  genpassu  7708  nqprloc  7728  ltaprlem  7801  recexprlemopl  7808  recexprlemopu  7810  recexprlemupu  7811  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemupu  7832  caucvgprlemupu  7855  caucvgprprlemupu  7883  archsr  7965  peano2nnnn  8036  receuap  8812  peano2nn  9118  nnaddcl  9126  zrevaddcl  9493  nzadd  9495  zdiv  9531  nneo  9546  zeo2  9549  peano5uzti  9551  fzind  9558  fnn0ind  9559  lbzbi  9807  qrevaddcl  9835  irradd  9837  irrmul  9838  ltsubrp  9882  ltaddrp  9883  xnn0xadd0  10059  icoshft  10182  fzen  10235  elfzm11  10283  uzsplit  10284  fzoval  10340  elfzom1elp1fzo  10403  exfzdc  10441  modaddmodup  10604  frec2uzrdg  10626  nninfinf  10660  seq3clss  10688  monoord  10702  seq3caopr3  10708  seqcaopr3g  10709  seq3f1olemp  10732  seqf1oglem2a  10735  seqf1og  10738  seq3id3  10741  seq3homo  10744  seq3z  10745  seqfeq4g  10748  ser3ge0  10753  expadd  10798  expmul  10801  leexp1a  10811  modqexp  10883  faccl  10952  facdiv  10955  faclbnd  10958  faclbnd6  10961  omgadd  11019  hashunsng  11024  seq3coll  11059  fundm2domnop0  11062  swrdswrdlem  11231  swrdswrd  11232  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccat3  11261  shftlem  11322  resqrexlemover  11516  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc3  11522  climub  11850  climserle  11851  fsumzcl2  11911  fsumsplitsnun  11925  fsum2d  11941  modfsummodlemstep  11963  fsumabs  11971  fsumiun  11983  bcxmas  11995  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  prodfap0  12051  prodfrecap  12052  ntrivcvgap  12054  prodmodc  12084  fprodssdc  12096  fprodabs  12122  fprod2d  12129  dvdsmod0  12299  dvds2ln  12330  dvdsabseq  12353  dvdsdivcl  12356  alzdvds  12360  oddnn02np1  12386  m1exp1  12407  nn0o1gt2  12411  nno  12412  ndvdsadd  12437  flodddiv4  12442  bitsinv1  12468  gcddiv  12535  gcdmultiple  12536  gcdmultiplez  12537  rplpwr  12543  dvdssq  12547  nninfct  12557  nn0seqcvgd  12558  alginv  12564  algcvga  12568  algfx  12569  isprm2  12634  isprm3  12635  prmdvdsexp  12665  eulerthlemrprm  12746  eulerthlema  12747  pcmpt  12861  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemhom  12981  omiunct  13010  nninfdclemlt  13017  setsn0fun  13064  mgmcl  13387  dfgrp3mlem  13626  mhmmulg  13695  resghm2b  13794  gsumfzconst  13873  srgpcomp  13948  lmodfopnelem1  14282  rmodislmodlem  14308  lss1d  14341  cnfldmulg  14534  cnfldexp  14535  gsumfzfsumlemm  14545  restopnb  14849  restdis  14852  tgcnp  14877  cnntr  14893  cnsscnp  14897  txcn  14943  txlm  14947  mettri  15041  blssexps  15097  blssex  15098  mopni3  15152  metss  15162  dvmptfsum  15393  plycolemc  15426  rpcxpmul2  15581  gausslemma2dlem6  15740  lgsquad2lem2  15755  2lgslem1c  15763  2lgslem3  15774  2lgs  15777  uhgredgrnv  15930  usgruspgrben  15978  usgredg2vlem2  16015  2spim  16088