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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  565  pm4.79dc  915  dedlema  982  dedlemb  983  19.35-1  1677  cbval2  1977  cbvex2  1978  nelelne  2512  r19.21be  2641  r19.35-1  2701  mosubt  3003  sbcrext  3129  uneqdifeqim  3613  ssuni  3957  uniss2  3966  elpwuni  4102  elssabg  4284  elpw2g  4292  epelg  4435  elomssom  4752  relop  4930  riinint  5043  cnviinm  5329  funopg  5411  fun  5561  tz6.12c  5725  fvelrnb  5750  fmptco  5874  funopsn  5891  fnressn  5901  fressnfv  5902  fvtp2g  5924  fvtp3g  5925  fconst2g  5930  isores3  6021  isoselem  6026  eloprabga  6175  fo1stresm  6395  poxp  6468  fsuppeq  6487  suppssdc  6500  brtpos2  6522  smores  6563  tfrlem1  6579  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  frecrdg  6679  oawordriexmid  6743  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nnmsucr  6761  nndifsnid  6780  nnmordi  6789  iinerm  6881  th3qlem2  6912  elpmg  6938  pmss12g  6956  mapsn  6972  brdomg  7032  f1domg  7044  ssdomg  7065  nndomo  7165  ffsuppbi  7300  elfi2  7306  nnnninfeq2  7469  carden2bex  7535  cc3  7634  addclpi  7694  addnidpig  7703  genpassl  7891  genpassu  7892  nqprloc  7912  ltaprlem  7985  recexprlemopl  7992  recexprlemopu  7994  recexprlemupu  7995  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemupu  8016  caucvgprlemupu  8039  caucvgprprlemupu  8067  archsr  8149  peano2nnnn  8220  receuap  9001  indval0  9299  peano2nn  9318  nnaddcl  9326  zrevaddcl  9699  nzadd  9701  zdiv  9738  nneo  9753  zeo2  9756  peano5uzti  9758  fzind  9765  fnn0ind  9766  lbzbi  10025  qrevaddcl  10053  irradd  10055  irrmul  10057  ltsubrp  10101  ltaddrp  10102  xnn0xadd0  10279  icoshft  10402  fzen  10457  elfzm11  10508  uzsplit  10509  fzoval  10565  elfzom1elp1fzo  10630  exfzdc  10669  modaddmodup  10837  frec2uzrdg  10859  nninfinf  10893  seq3clss  10921  monoord  10935  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemp  10965  seqf1oglem2a  10968  seqf1og  10971  seq3id3  10974  seq3homo  10977  seq3z  10978  seqfeq4g  10981  ser3ge0  10986  expadd  11031  expmul  11034  leexp1a  11044  modqexp  11117  faccl  11187  facdiv  11190  faclbnd  11193  faclbnd6  11196  omgadd  11256  hashunsng  11262  hashmap  11282  hashf1  11301  seq3coll  11308  fundm2domnop0  11314  swrdswrdlem  11490  swrdswrd  11491  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccat3  11520  shftlem  11595  resqrexlemover  11790  resqrexlemdecn  11792  resqrexlemlo  11793  resqrexlemcalc3  11796  climub  12126  climserle  12127  fsumzcl2  12188  fsumsplitsnun  12202  fsum2d  12218  modfsummodlemstep  12240  fsumabs  12248  fsumiun  12260  bcxmas  12272  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  prodfap0  12328  prodfrecap  12329  ntrivcvgap  12331  prodmodc  12361  fprodssdc  12373  fprodabs  12399  fprod2d  12406  dvdsmod0  12576  dvds2ln  12607  dvdsabseq  12630  dvdsdivcl  12633  alzdvds  12637  oddnn02np1  12663  m1exp1  12684  nn0o1gt2  12688  nno  12689  ndvdsadd  12714  flodddiv4  12719  bitsinv1  12745  gcddiv  12812  gcdmultiple  12813  gcdmultiplez  12814  rplpwr  12820  dvdssq  12824  nninfct  12834  nn0seqcvgd  12835  alginv  12841  algcvga  12845  algfx  12846  isprm2  12911  isprm3  12912  prmdvdsexp  12943  eulerthlemrprm  13027  eulerthlema  13028  pcmpt  13142  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemhom  13355  omiunct  13384  nninfdclemlt  13391  setsn0fun  13438  mgmcl  13728  dfgrp3mlem  13952  mhmmulg  14015  resghm2b  14114  gzsumconst  14192  srgpcomp  14343  lmodfopnelem1  14710  rmodislmodlem  14736  lss1d  14769  cnfldmulg  14962  cnfldexp  14963  restopnb  15331  restdis  15334  tgcnp  15359  cnntr  15375  cnsscnp  15379  txcn  15425  txlm  15429  mettri  15523  blssexps  15579  blssex  15580  mopni3  15634  metss  15644  dvmptfsum  15875  plycolemc  15908  rpcxpmul2  16068  ppiqub  16194  bcmono  16202  bpos1lem  16207  bposlem5  16213  gausslemma2dlem6  16284  lgsquad2lem2  16299  2lgslem1c  16307  2lgslem3  16318  2lgs  16321  uhgredgrnv  16477  usgruspgrben  16525  usgredg2vlem2  16562  subupgr  16612  uspgr2wlkeq  16704  clwwlkccatlem  16739  umgrclwwlkge2  16741  clwwlkn1loopb  16759  clwwlknonex2lem2  16777  eupth2lem3lem4fi  16812  eupth2fi  16818  2spim  16892  exmidcon  17135  alsralrex  17251