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  958  dedlemb  959  19.35-1  1611  cbval2  1908  cbvex2  1909  nelelne  2426  r19.21be  2555  r19.35-1  2614  mosubt  2898  sbcrext  3023  uneqdifeqim  3489  ssuni  3805  uniss2  3814  elpwuni  3949  elssabg  4121  elpw2g  4129  epelg  4262  elomssom  4576  relop  4748  riinint  4859  cnviinm  5139  funopg  5216  fun  5354  tz6.12c  5510  fvelrnb  5528  fmptco  5645  fnressn  5665  fressnfv  5666  fvtp2g  5688  fvtp3g  5689  fconst2g  5694  isores3  5777  isoselem  5782  eloprabga  5920  fo1stresm  6121  poxp  6191  brtpos2  6210  smores  6251  tfrlem1  6267  tfrlemi1  6291  tfr1onlemaccex  6307  tfrcllemaccex  6320  frecrdg  6367  oawordriexmid  6429  nnacl  6439  nnmcl  6440  nnacom  6443  nnaass  6444  nnmsucr  6447  nndifsnid  6466  nnmordi  6475  iinerm  6564  th3qlem2  6595  elpmg  6621  pmss12g  6632  mapsn  6647  brdomg  6705  f1domg  6715  ssdomg  6735  nndomo  6821  elfi2  6928  nnnninfeq2  7084  carden2bex  7136  cc3  7200  addclpi  7259  addnidpig  7268  genpassl  7456  genpassu  7457  nqprloc  7477  ltaprlem  7550  recexprlemopl  7557  recexprlemopu  7559  recexprlemupu  7560  recexprlemss1l  7567  recexprlemss1u  7568  cauappcvgprlemupu  7581  caucvgprlemupu  7604  caucvgprprlemupu  7632  archsr  7714  peano2nnnn  7785  receuap  8557  peano2nn  8860  nnaddcl  8868  zrevaddcl  9232  nzadd  9234  zdiv  9270  nneo  9285  zeo2  9288  peano5uzti  9290  fzind  9297  fnn0ind  9298  lbzbi  9545  qrevaddcl  9573  irradd  9575  irrmul  9576  ltsubrp  9617  ltaddrp  9618  xnn0xadd0  9794  icoshft  9917  fzen  9968  elfzm11  10016  uzsplit  10017  fzoval  10073  elfzom1elp1fzo  10127  exfzdc  10165  modaddmodup  10312  frec2uzrdg  10334  seq3clss  10392  monoord  10401  seq3caopr3  10406  seq3f1olemp  10427  seq3id3  10432  seq3homo  10435  seq3z  10436  ser3ge0  10442  expadd  10487  expmul  10490  leexp1a  10500  modqexp  10570  faccl  10637  facdiv  10640  faclbnd  10643  faclbnd6  10646  omgadd  10704  hashunsng  10709  seq3coll  10741  shftlem  10744  resqrexlemover  10938  resqrexlemdecn  10940  resqrexlemlo  10941  resqrexlemcalc3  10944  climub  11271  climserle  11272  fsumzcl2  11332  fsumsplitsnun  11346  fsum2d  11362  modfsummodlemstep  11384  fsumabs  11392  fsumiun  11404  bcxmas  11416  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  prodfap0  11472  prodfrecap  11473  ntrivcvgap  11475  prodmodc  11505  fprodssdc  11517  fprodabs  11543  fprod2d  11550  dvdsmod0  11719  dvds2ln  11750  dvdsabseq  11770  dvdsdivcl  11773  alzdvds  11777  oddnn02np1  11802  m1exp1  11823  nn0o1gt2  11827  nno  11828  ndvdsadd  11853  flodddiv4  11856  gcddiv  11937  gcdmultiple  11938  gcdmultiplez  11939  rplpwr  11945  dvdssq  11949  nn0seqcvgd  11952  alginv  11958  algcvga  11962  algfx  11963  isprm2  12028  isprm3  12029  prmdvdsexp  12057  eulerthlemrprm  12138  eulerthlema  12139  pcmpt  12250  ennnfoneleminc  12281  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemhom  12285  omiunct  12314  nninfdclemlt  12323  setsn0fun  12368  restopnb  12722  restdis  12725  tgcnp  12750  cnntr  12766  cnsscnp  12770  txcn  12816  txlm  12820  mettri  12914  blssexps  12970  blssex  12971  mopni3  13025  metss  13035  2spim  13482