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  548  pm4.79dc  888  dedlema  953  dedlemb  954  19.35-1  1603  cbval2  1891  cbvex2  1892  nelelne  2398  r19.21be  2521  r19.35-1  2579  mosubt  2856  sbcrext  2981  uneqdifeqim  3443  ssuni  3753  uniss2  3762  elpwuni  3897  elssabg  4068  elpw2g  4076  epelg  4207  elnn  4514  relop  4684  riinint  4795  cnviinm  5075  funopg  5152  fun  5290  tz6.12c  5444  fvelrnb  5462  fmptco  5579  fnressn  5599  fressnfv  5600  fvtp2g  5622  fvtp3g  5623  fconst2g  5628  isores3  5709  isoselem  5714  eloprabga  5851  fo1stresm  6052  poxp  6122  brtpos2  6141  smores  6182  tfrlem1  6198  tfrlemi1  6222  tfr1onlemaccex  6238  tfrcllemaccex  6251  frecrdg  6298  oawordriexmid  6359  nnacl  6369  nnmcl  6370  nnacom  6373  nnaass  6374  nnmsucr  6377  nndifsnid  6396  nnmordi  6405  iinerm  6494  th3qlem2  6525  elpmg  6551  pmss12g  6562  mapsn  6577  brdomg  6635  f1domg  6645  ssdomg  6665  nndomo  6751  elfi2  6853  carden2bex  7038  addclpi  7128  addnidpig  7137  genpassl  7325  genpassu  7326  nqprloc  7346  ltaprlem  7419  recexprlemopl  7426  recexprlemopu  7428  recexprlemupu  7429  recexprlemss1l  7436  recexprlemss1u  7437  cauappcvgprlemupu  7450  caucvgprlemupu  7473  caucvgprprlemupu  7501  archsr  7583  peano2nnnn  7654  receuap  8423  peano2nn  8725  nnaddcl  8733  zrevaddcl  9097  nzadd  9099  zdiv  9132  nneo  9147  zeo2  9150  peano5uzti  9152  fzind  9159  fnn0ind  9160  lbzbi  9401  qrevaddcl  9429  irradd  9431  irrmul  9432  ltsubrp  9471  ltaddrp  9472  xnn0xadd0  9643  icoshft  9766  fzen  9816  elfzm11  9864  uzsplit  9865  fzoval  9918  elfzom1elp1fzo  9972  exfzdc  10010  modaddmodup  10153  frec2uzrdg  10175  seq3clss  10233  monoord  10242  seq3caopr3  10247  seq3f1olemp  10268  seq3id3  10273  seq3homo  10276  seq3z  10277  ser3ge0  10283  expadd  10328  expmul  10331  leexp1a  10341  faccl  10474  facdiv  10477  faclbnd  10480  faclbnd6  10483  omgadd  10541  hashunsng  10546  seq3coll  10578  shftlem  10581  resqrexlemover  10775  resqrexlemdecn  10777  resqrexlemlo  10778  resqrexlemcalc3  10781  climub  11106  climserle  11107  fsumzcl2  11167  fsumsplitsnun  11181  fsum2d  11197  modfsummodlemstep  11219  fsumabs  11227  fsumiun  11239  bcxmas  11251  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  prodfap0  11307  prodfrecap  11308  ntrivcvgap  11310  dvds2ln  11515  dvdsabseq  11534  dvdsdivcl  11537  alzdvds  11541  oddnn02np1  11566  m1exp1  11587  nn0o1gt2  11591  nno  11592  ndvdsadd  11617  flodddiv4  11620  gcddiv  11696  gcdmultiple  11697  gcdmultiplez  11698  rplpwr  11704  dvdssq  11708  nn0seqcvgd  11711  alginv  11717  algcvga  11721  algfx  11722  isprm2  11787  isprm3  11788  prmdvdsexp  11815  ennnfoneleminc  11913  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemhom  11917  setsn0fun  11985  restopnb  12339  restdis  12342  tgcnp  12367  cnntr  12383  cnsscnp  12387  txcn  12433  txlm  12437  mettri  12531  blssexps  12587  blssex  12588  mopni3  12642  metss  12652  2spim  12962