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  8999  indval0  9297  peano2nn  9316  nnaddcl  9324  zrevaddcl  9695  nzadd  9697  zdiv  9734  nneo  9749  zeo2  9752  peano5uzti  9754  fzind  9761  fnn0ind  9762  lbzbi  10016  qrevaddcl  10044  irradd  10046  irrmul  10047  ltsubrp  10091  ltaddrp  10092  xnn0xadd0  10269  icoshft  10392  fzen  10447  elfzm11  10498  uzsplit  10499  fzoval  10555  elfzom1elp1fzo  10620  exfzdc  10659  modaddmodup  10824  frec2uzrdg  10846  nninfinf  10880  seq3clss  10908  monoord  10922  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemp  10952  seqf1oglem2a  10955  seqf1og  10958  seq3id3  10961  seq3homo  10964  seq3z  10965  seqfeq4g  10968  ser3ge0  10973  expadd  11018  expmul  11021  leexp1a  11031  modqexp  11104  faccl  11173  facdiv  11176  faclbnd  11179  faclbnd6  11182  omgadd  11242  hashunsng  11248  hashmap  11268  hashf1  11287  seq3coll  11294  fundm2domnop0  11300  swrdswrdlem  11476  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccat3  11506  shftlem  11581  resqrexlemover  11776  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc3  11782  climub  12110  climserle  12111  fsumzcl2  12172  fsumsplitsnun  12186  fsum2d  12202  modfsummodlemstep  12224  fsumabs  12232  fsumiun  12244  bcxmas  12256  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  prodfap0  12312  prodfrecap  12313  ntrivcvgap  12315  prodmodc  12345  fprodssdc  12357  fprodabs  12383  fprod2d  12390  dvdsmod0  12560  dvds2ln  12591  dvdsabseq  12614  dvdsdivcl  12617  alzdvds  12621  oddnn02np1  12647  m1exp1  12668  nn0o1gt2  12672  nno  12673  ndvdsadd  12698  flodddiv4  12703  bitsinv1  12729  gcddiv  12796  gcdmultiple  12797  gcdmultiplez  12798  rplpwr  12804  dvdssq  12808  nninfct  12818  nn0seqcvgd  12819  alginv  12825  algcvga  12829  algfx  12830  isprm2  12895  isprm3  12896  prmdvdsexp  12926  eulerthlemrprm  13007  eulerthlema  13008  pcmpt  13122  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemhom  13306  omiunct  13335  nninfdclemlt  13342  setsn0fun  13389  mgmcl  13679  dfgrp3mlem  13903  mhmmulg  13966  resghm2b  14065  gzsumconst  14143  srgpcomp  14294  lmodfopnelem1  14661  rmodislmodlem  14687  lss1d  14720  cnfldmulg  14913  cnfldexp  14914  restopnb  15282  restdis  15285  tgcnp  15310  cnntr  15326  cnsscnp  15330  txcn  15376  txlm  15380  mettri  15474  blssexps  15530  blssex  15531  mopni3  15585  metss  15595  dvmptfsum  15826  plycolemc  15859  rpcxpmul2  16015  gausslemma2dlem6  16186  lgsquad2lem2  16201  2lgslem1c  16209  2lgslem3  16220  2lgs  16223  uhgredgrnv  16379  usgruspgrben  16427  usgredg2vlem2  16464  subupgr  16514  uspgr2wlkeq  16606  clwwlkccatlem  16641  umgrclwwlkge2  16643  clwwlkn1loopb  16661  clwwlknonex2lem2  16679  eupth2lem3lem4fi  16714  eupth2fi  16720  2spim  16794  exmidcon  17037  alsralrex  17153