Theorem expcom 115

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 114	. 2 |- ( ph -> ( ps -> ch ) )
3	2	com12 30	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  ancoms  266  syldan  280  sylan  281  animpimp2impd  549  pm4.79dc  893  dedlema  959  dedlemb  960  19.35-1  1612  cbval2  1909  cbvex2  1910  nelelne  2428  r19.21be  2557  r19.35-1  2616  mosubt  2903  sbcrext  3028  uneqdifeqim  3494  ssuni  3811  uniss2  3820  elpwuni  3955  elssabg  4127  elpw2g  4135  epelg  4268  elomssom  4582  relop  4754  riinint  4865  cnviinm  5145  funopg  5222  fun  5360  tz6.12c  5516  fvelrnb  5534  fmptco  5651  fnressn  5671  fressnfv  5672  fvtp2g  5694  fvtp3g  5695  fconst2g  5700  isores3  5783  isoselem  5788  eloprabga  5929  fo1stresm  6129  poxp  6200  brtpos2  6219  smores  6260  tfrlem1  6276  tfrlemi1  6300  tfr1onlemaccex  6316  tfrcllemaccex  6329  frecrdg  6376  oawordriexmid  6438  nnacl  6448  nnmcl  6449  nnacom  6452  nnaass  6453  nnmsucr  6456  nndifsnid  6475  nnmordi  6484  iinerm  6573  th3qlem2  6604  elpmg  6630  pmss12g  6641  mapsn  6656  brdomg  6714  f1domg  6724  ssdomg  6744  nndomo  6830  elfi2  6937  nnnninfeq2  7093  carden2bex  7145  cc3  7209  addclpi  7268  addnidpig  7277  genpassl  7465  genpassu  7466  nqprloc  7486  ltaprlem  7559  recexprlemopl  7566  recexprlemopu  7568  recexprlemupu  7569  recexprlemss1l  7576  recexprlemss1u  7577  cauappcvgprlemupu  7590  caucvgprlemupu  7613  caucvgprprlemupu  7641  archsr  7723  peano2nnnn  7794  receuap  8566  peano2nn  8869  nnaddcl  8877  zrevaddcl  9241  nzadd  9243  zdiv  9279  nneo  9294  zeo2  9297  peano5uzti  9299  fzind  9306  fnn0ind  9307  lbzbi  9554  qrevaddcl  9582  irradd  9584  irrmul  9585  ltsubrp  9626  ltaddrp  9627  xnn0xadd0  9803  icoshft  9926  fzen  9978  elfzm11  10026  uzsplit  10027  fzoval  10083  elfzom1elp1fzo  10137  exfzdc  10175  modaddmodup  10322  frec2uzrdg  10344  seq3clss  10402  monoord  10411  seq3caopr3  10416  seq3f1olemp  10437  seq3id3  10442  seq3homo  10445  seq3z  10446  ser3ge0  10452  expadd  10497  expmul  10500  leexp1a  10510  modqexp  10581  faccl  10648  facdiv  10651  faclbnd  10654  faclbnd6  10657  omgadd  10715  hashunsng  10720  seq3coll  10755  shftlem  10758  resqrexlemover  10952  resqrexlemdecn  10954  resqrexlemlo  10955  resqrexlemcalc3  10958  climub  11285  climserle  11286  fsumzcl2  11346  fsumsplitsnun  11360  fsum2d  11376  modfsummodlemstep  11398  fsumabs  11406  fsumiun  11418  bcxmas  11430  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  prodfap0  11486  prodfrecap  11487  ntrivcvgap  11489  prodmodc  11519  fprodssdc  11531  fprodabs  11557  fprod2d  11564  dvdsmod0  11733  dvds2ln  11764  dvdsabseq  11785  dvdsdivcl  11788  alzdvds  11792  oddnn02np1  11817  m1exp1  11838  nn0o1gt2  11842  nno  11843  ndvdsadd  11868  flodddiv4  11871  gcddiv  11952  gcdmultiple  11953  gcdmultiplez  11954  rplpwr  11960  dvdssq  11964  nn0seqcvgd  11973  alginv  11979  algcvga  11983  algfx  11984  isprm2  12049  isprm3  12050  prmdvdsexp  12080  eulerthlemrprm  12161  eulerthlema  12162  pcmpt  12273  ennnfoneleminc  12344  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemhom  12348  omiunct  12377  nninfdclemlt  12384  setsn0fun  12431  mgmcl  12590  restopnb  12821  restdis  12824  tgcnp  12849  cnntr  12865  cnsscnp  12869  txcn  12915  txlm  12919  mettri  13013  blssexps  13069  blssex  13070  mopni3  13124  metss  13134  2spim  13647