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  1647  cbval2  1945  cbvex2  1946  nelelne  2468  r19.21be  2597  r19.35-1  2656  mosubt  2950  sbcrext  3076  uneqdifeqim  3546  ssuni  3872  uniss2  3881  elpwuni  4017  elssabg  4192  elpw2g  4200  epelg  4337  elomssom  4653  relop  4828  riinint  4939  cnviinm  5224  funopg  5305  fun  5448  tz6.12c  5606  fvelrnb  5626  fmptco  5746  funopsn  5762  fnressn  5770  fressnfv  5771  fvtp2g  5793  fvtp3g  5794  fconst2g  5799  isores3  5884  isoselem  5889  eloprabga  6032  fo1stresm  6247  poxp  6318  brtpos2  6337  smores  6378  tfrlem1  6394  tfrlemi1  6418  tfr1onlemaccex  6434  tfrcllemaccex  6447  frecrdg  6494  oawordriexmid  6556  nnacl  6566  nnmcl  6567  nnacom  6570  nnaass  6571  nnmsucr  6574  nndifsnid  6593  nnmordi  6602  iinerm  6694  th3qlem2  6725  elpmg  6751  pmss12g  6762  mapsn  6777  brdomg  6837  f1domg  6849  ssdomg  6870  nndomo  6961  elfi2  7074  nnnninfeq2  7231  carden2bex  7297  cc3  7380  addclpi  7440  addnidpig  7449  genpassl  7637  genpassu  7638  nqprloc  7658  ltaprlem  7731  recexprlemopl  7738  recexprlemopu  7740  recexprlemupu  7741  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemupu  7762  caucvgprlemupu  7785  caucvgprprlemupu  7813  archsr  7895  peano2nnnn  7966  receuap  8742  peano2nn  9048  nnaddcl  9056  zrevaddcl  9423  nzadd  9425  zdiv  9461  nneo  9476  zeo2  9479  peano5uzti  9481  fzind  9488  fnn0ind  9489  lbzbi  9737  qrevaddcl  9765  irradd  9767  irrmul  9768  ltsubrp  9812  ltaddrp  9813  xnn0xadd0  9989  icoshft  10112  fzen  10165  elfzm11  10213  uzsplit  10214  fzoval  10270  elfzom1elp1fzo  10331  exfzdc  10369  modaddmodup  10532  frec2uzrdg  10554  nninfinf  10588  seq3clss  10616  monoord  10630  seq3caopr3  10636  seqcaopr3g  10637  seq3f1olemp  10660  seqf1oglem2a  10663  seqf1og  10666  seq3id3  10669  seq3homo  10672  seq3z  10673  seqfeq4g  10676  ser3ge0  10681  expadd  10726  expmul  10729  leexp1a  10739  modqexp  10811  faccl  10880  facdiv  10883  faclbnd  10886  faclbnd6  10889  omgadd  10947  hashunsng  10952  seq3coll  10987  fundm2domnop0  10990  shftlem  11127  resqrexlemover  11321  resqrexlemdecn  11323  resqrexlemlo  11324  resqrexlemcalc3  11327  climub  11655  climserle  11656  fsumzcl2  11716  fsumsplitsnun  11730  fsum2d  11746  modfsummodlemstep  11768  fsumabs  11776  fsumiun  11788  bcxmas  11800  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  prodfap0  11856  prodfrecap  11857  ntrivcvgap  11859  prodmodc  11889  fprodssdc  11901  fprodabs  11927  fprod2d  11934  dvdsmod0  12104  dvds2ln  12135  dvdsabseq  12158  dvdsdivcl  12161  alzdvds  12165  oddnn02np1  12191  m1exp1  12212  nn0o1gt2  12216  nno  12217  ndvdsadd  12242  flodddiv4  12247  bitsinv1  12273  gcddiv  12340  gcdmultiple  12341  gcdmultiplez  12342  rplpwr  12348  dvdssq  12352  nninfct  12362  nn0seqcvgd  12363  alginv  12369  algcvga  12373  algfx  12374  isprm2  12439  isprm3  12440  prmdvdsexp  12470  eulerthlemrprm  12551  eulerthlema  12552  pcmpt  12666  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemhom  12786  omiunct  12815  nninfdclemlt  12822  setsn0fun  12869  mgmcl  13191  dfgrp3mlem  13430  mhmmulg  13499  resghm2b  13598  gsumfzconst  13677  srgpcomp  13752  lmodfopnelem1  14086  rmodislmodlem  14112  lss1d  14145  cnfldmulg  14338  cnfldexp  14339  gsumfzfsumlemm  14349  restopnb  14653  restdis  14656  tgcnp  14681  cnntr  14697  cnsscnp  14701  txcn  14747  txlm  14751  mettri  14845  blssexps  14901  blssex  14902  mopni3  14956  metss  14966  dvmptfsum  15197  plycolemc  15230  rpcxpmul2  15385  gausslemma2dlem6  15544  lgsquad2lem2  15559  2lgslem1c  15567  2lgslem3  15578  2lgs  15581  2spim  15702