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  908  dedlema  975  dedlemb  976  19.35-1  1670  cbval2  1968  cbvex2  1969  nelelne  2492  r19.21be  2621  r19.35-1  2681  mosubt  2980  sbcrext  3106  uneqdifeqim  3577  ssuni  3910  uniss2  3919  elpwuni  4055  elssabg  4232  elpw2g  4240  epelg  4381  elomssom  4697  relop  4872  riinint  4985  cnviinm  5270  funopg  5352  fun  5499  tz6.12c  5659  fvelrnb  5683  fmptco  5803  funopsn  5819  fnressn  5829  fressnfv  5830  fvtp2g  5852  fvtp3g  5853  fconst2g  5858  isores3  5945  isoselem  5950  eloprabga  6097  fo1stresm  6313  poxp  6384  brtpos2  6403  smores  6444  tfrlem1  6460  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  frecrdg  6560  oawordriexmid  6624  nnacl  6634  nnmcl  6635  nnacom  6638  nnaass  6639  nnmsucr  6642  nndifsnid  6661  nnmordi  6670  iinerm  6762  th3qlem2  6793  elpmg  6819  pmss12g  6830  mapsn  6845  brdomg  6905  f1domg  6917  ssdomg  6938  nndomo  7033  elfi2  7150  nnnninfeq2  7307  carden2bex  7373  cc3  7465  addclpi  7525  addnidpig  7534  genpassl  7722  genpassu  7723  nqprloc  7743  ltaprlem  7816  recexprlemopl  7823  recexprlemopu  7825  recexprlemupu  7826  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemupu  7847  caucvgprlemupu  7870  caucvgprprlemupu  7898  archsr  7980  peano2nnnn  8051  receuap  8827  peano2nn  9133  nnaddcl  9141  zrevaddcl  9508  nzadd  9510  zdiv  9546  nneo  9561  zeo2  9564  peano5uzti  9566  fzind  9573  fnn0ind  9574  lbzbi  9823  qrevaddcl  9851  irradd  9853  irrmul  9854  ltsubrp  9898  ltaddrp  9899  xnn0xadd0  10075  icoshft  10198  fzen  10251  elfzm11  10299  uzsplit  10300  fzoval  10356  elfzom1elp1fzo  10420  exfzdc  10458  modaddmodup  10621  frec2uzrdg  10643  nninfinf  10677  seq3clss  10705  monoord  10719  seq3caopr3  10725  seqcaopr3g  10726  seq3f1olemp  10749  seqf1oglem2a  10752  seqf1og  10755  seq3id3  10758  seq3homo  10761  seq3z  10762  seqfeq4g  10765  ser3ge0  10770  expadd  10815  expmul  10818  leexp1a  10828  modqexp  10900  faccl  10969  facdiv  10972  faclbnd  10975  faclbnd6  10978  omgadd  11036  hashunsng  11042  seq3coll  11077  fundm2domnop0  11080  swrdswrdlem  11251  swrdswrd  11252  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccat3  11281  shftlem  11342  resqrexlemover  11536  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc3  11542  climub  11870  climserle  11871  fsumzcl2  11931  fsumsplitsnun  11945  fsum2d  11961  modfsummodlemstep  11983  fsumabs  11991  fsumiun  12003  bcxmas  12015  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  prodfap0  12071  prodfrecap  12072  ntrivcvgap  12074  prodmodc  12104  fprodssdc  12116  fprodabs  12142  fprod2d  12149  dvdsmod0  12319  dvds2ln  12350  dvdsabseq  12373  dvdsdivcl  12376  alzdvds  12380  oddnn02np1  12406  m1exp1  12427  nn0o1gt2  12431  nno  12432  ndvdsadd  12457  flodddiv4  12462  bitsinv1  12488  gcddiv  12555  gcdmultiple  12556  gcdmultiplez  12557  rplpwr  12563  dvdssq  12567  nninfct  12577  nn0seqcvgd  12578  alginv  12584  algcvga  12588  algfx  12589  isprm2  12654  isprm3  12655  prmdvdsexp  12685  eulerthlemrprm  12766  eulerthlema  12767  pcmpt  12881  ennnfoneleminc  12997  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemhom  13001  omiunct  13030  nninfdclemlt  13037  setsn0fun  13084  mgmcl  13407  dfgrp3mlem  13646  mhmmulg  13715  resghm2b  13814  gsumfzconst  13893  srgpcomp  13968  lmodfopnelem1  14303  rmodislmodlem  14329  lss1d  14362  cnfldmulg  14555  cnfldexp  14556  gsumfzfsumlemm  14566  restopnb  14870  restdis  14873  tgcnp  14898  cnntr  14914  cnsscnp  14918  txcn  14964  txlm  14968  mettri  15062  blssexps  15118  blssex  15119  mopni3  15173  metss  15183  dvmptfsum  15414  plycolemc  15447  rpcxpmul2  15602  gausslemma2dlem6  15761  lgsquad2lem2  15776  2lgslem1c  15784  2lgslem3  15795  2lgs  15798  uhgredgrnv  15951  usgruspgrben  15999  usgredg2vlem2  16036  uspgr2wlkeq  16106  clwwlkccatlem  16137  umgrclwwlkge2  16139  2spim  16185