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  554  pm4.79dc  898  dedlema  964  dedlemb  965  19.35-1  1617  cbval2  1914  cbvex2  1915  nelelne  2432  r19.21be  2561  r19.35-1  2620  mosubt  2907  sbcrext  3032  uneqdifeqim  3500  ssuni  3818  uniss2  3827  elpwuni  3962  elssabg  4134  elpw2g  4142  epelg  4275  elomssom  4589  relop  4761  riinint  4872  cnviinm  5152  funopg  5232  fun  5370  tz6.12c  5526  fvelrnb  5544  fmptco  5662  fnressn  5682  fressnfv  5683  fvtp2g  5705  fvtp3g  5706  fconst2g  5711  isores3  5794  isoselem  5799  eloprabga  5940  fo1stresm  6140  poxp  6211  brtpos2  6230  smores  6271  tfrlem1  6287  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  frecrdg  6387  oawordriexmid  6449  nnacl  6459  nnmcl  6460  nnacom  6463  nnaass  6464  nnmsucr  6467  nndifsnid  6486  nnmordi  6495  iinerm  6585  th3qlem2  6616  elpmg  6642  pmss12g  6653  mapsn  6668  brdomg  6726  f1domg  6736  ssdomg  6756  nndomo  6842  elfi2  6949  nnnninfeq2  7105  carden2bex  7166  cc3  7230  addclpi  7289  addnidpig  7298  genpassl  7486  genpassu  7487  nqprloc  7507  ltaprlem  7580  recexprlemopl  7587  recexprlemopu  7589  recexprlemupu  7590  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemupu  7611  caucvgprlemupu  7634  caucvgprprlemupu  7662  archsr  7744  peano2nnnn  7815  receuap  8587  peano2nn  8890  nnaddcl  8898  zrevaddcl  9262  nzadd  9264  zdiv  9300  nneo  9315  zeo2  9318  peano5uzti  9320  fzind  9327  fnn0ind  9328  lbzbi  9575  qrevaddcl  9603  irradd  9605  irrmul  9606  ltsubrp  9647  ltaddrp  9648  xnn0xadd0  9824  icoshft  9947  fzen  9999  elfzm11  10047  uzsplit  10048  fzoval  10104  elfzom1elp1fzo  10158  exfzdc  10196  modaddmodup  10343  frec2uzrdg  10365  seq3clss  10423  monoord  10432  seq3caopr3  10437  seq3f1olemp  10458  seq3id3  10463  seq3homo  10466  seq3z  10467  ser3ge0  10473  expadd  10518  expmul  10521  leexp1a  10531  modqexp  10602  faccl  10669  facdiv  10672  faclbnd  10675  faclbnd6  10678  omgadd  10737  hashunsng  10742  seq3coll  10777  shftlem  10780  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc3  10980  climub  11307  climserle  11308  fsumzcl2  11368  fsumsplitsnun  11382  fsum2d  11398  modfsummodlemstep  11420  fsumabs  11428  fsumiun  11440  bcxmas  11452  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  prodfap0  11508  prodfrecap  11509  ntrivcvgap  11511  prodmodc  11541  fprodssdc  11553  fprodabs  11579  fprod2d  11586  dvdsmod0  11755  dvds2ln  11786  dvdsabseq  11807  dvdsdivcl  11810  alzdvds  11814  oddnn02np1  11839  m1exp1  11860  nn0o1gt2  11864  nno  11865  ndvdsadd  11890  flodddiv4  11893  gcddiv  11974  gcdmultiple  11975  gcdmultiplez  11976  rplpwr  11982  dvdssq  11986  nn0seqcvgd  11995  alginv  12001  algcvga  12005  algfx  12006  isprm2  12071  isprm3  12072  prmdvdsexp  12102  eulerthlemrprm  12183  eulerthlema  12184  pcmpt  12295  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  omiunct  12399  nninfdclemlt  12406  setsn0fun  12453  mgmcl  12613  restopnb  12975  restdis  12978  tgcnp  13003  cnntr  13019  cnsscnp  13023  txcn  13069  txlm  13073  mettri  13167  blssexps  13223  blssex  13224  mopni3  13278  metss  13288  2spim  13801