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  7470  carden2bex  7536  cc3  7635  addclpi  7695  addnidpig  7704  genpassl  7892  genpassu  7893  nqprloc  7913  ltaprlem  7986  recexprlemopl  7993  recexprlemopu  7995  recexprlemupu  7996  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemupu  8017  caucvgprlemupu  8040  caucvgprprlemupu  8068  archsr  8150  peano2nnnn  8221  receuap  9002  indval0  9300  peano2nn  9319  nnaddcl  9327  zrevaddcl  9700  nzadd  9702  zdiv  9739  nneo  9754  zeo2  9757  peano5uzti  9759  fzind  9766  fnn0ind  9767  lbzbi  10026  qrevaddcl  10054  irradd  10056  irrmul  10058  ltsubrp  10102  ltaddrp  10103  xnn0xadd0  10280  icoshft  10403  fzen  10458  elfzm11  10509  uzsplit  10510  fzoval  10566  elfzom1elp1fzo  10631  exfzdc  10670  modaddmodup  10839  frec2uzrdg  10861  nninfinf  10895  seq3clss  10923  monoord  10937  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemp  10967  seqf1oglem2a  10970  seqf1og  10973  seq3id3  10976  seq3homo  10979  seq3z  10980  seqfeq4g  10983  ser3ge0  10988  expadd  11033  expmul  11036  leexp1a  11046  modqexp  11119  faccl  11189  facdiv  11192  faclbnd  11195  faclbnd6  11198  omgadd  11258  hashunsng  11264  hashmap  11284  hashf1  11303  seq3coll  11310  fundm2domnop0  11316  swrdswrdlem  11492  swrdswrd  11493  wrd2ind  11511  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccat3  11522  shftlem  11597  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc3  11798  climub  12129  climserle  12130  fsumzcl2  12191  fsumsplitsnun  12205  fsum2d  12221  modfsummodlemstep  12243  fsumabs  12251  fsumiun  12263  bcxmas  12275  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  prodfap0  12331  prodfrecap  12332  ntrivcvgap  12334  prodmodc  12364  fprodssdc  12376  fprodabs  12402  fprod2d  12409  dvdsmod0  12579  dvds2ln  12610  dvdsabseq  12633  dvdsdivcl  12636  alzdvds  12640  oddnn02np1  12666  m1exp1  12687  nn0o1gt2  12691  nno  12692  ndvdsadd  12717  flodddiv4  12722  bitsinv1  12748  gcddiv  12815  gcdmultiple  12816  gcdmultiplez  12817  rplpwr  12823  dvdssq  12827  nninfct  12837  nn0seqcvgd  12838  alginv  12844  algcvga  12848  algfx  12849  isprm2  12914  isprm3  12915  prmdvdsexp  12946  eulerthlemrprm  13030  eulerthlema  13031  pcmpt  13145  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemhom  13358  omiunct  13387  nninfdclemlt  13394  setsn0fun  13441  mgmcl  13732  dfgrp3mlem  13956  mhmmulg  14019  resghm2b  14118  cntzval  14147  gzsumconst  14227  srgpcomp  14378  lmodfopnelem1  14745  rmodislmodlem  14771  lss1d  14804  cnfldmulg  14997  cnfldexp  14998  restopnb  15373  restdis  15376  tgcnp  15401  cnntr  15417  cnsscnp  15421  txcn  15467  txlm  15471  mettri  15565  blssexps  15621  blssex  15622  mopni3  15676  metss  15686  dvmptfsum  15917  plycolemc  15950  rpcxpmul2  16110  ppiqub  16254  bcmono  16265  bpos1lem  16270  bposlem5  16276  gausslemma2dlem6  16352  lgsquad2lem2  16367  2lgslem1c  16375  2lgslem3  16386  2lgs  16389  uhgredgrnv  16545  usgruspgrben  16593  usgredg2vlem2  16630  subupgr  16680  uspgr2wlkeq  16772  clwwlkccatlem  16807  umgrclwwlkge2  16809  clwwlkn1loopb  16827  clwwlknonex2lem2  16845  eupth2lem3lem4fi  16880  eupth2fi  16886  2spim  16960  exmidcon  17203  alsralrex  17320