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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  ancoms  266  syldan  278  sylan  279  animpimp2impd  529  pm4.79dc  853  dedlema  921  dedlemb  922  19.35-1  1571  cbval2  1856  cbvex2  1857  nelelne  2359  r19.21be  2482  r19.35-1  2539  mosubt  2814  sbcrext  2938  uneqdifeqim  3395  ssuni  3705  uniss2  3714  elpwuni  3848  elssabg  4013  elpw2g  4021  epelg  4150  elnn  4457  relop  4627  riinint  4736  cnviinm  5016  funopg  5093  fun  5231  tz6.12c  5383  fvelrnb  5401  fmptco  5518  fnressn  5538  fressnfv  5539  fvtp2g  5561  fvtp3g  5562  fconst2g  5567  isores3  5648  isoselem  5653  eloprabga  5790  fo1stresm  5990  poxp  6059  brtpos2  6078  smores  6119  tfrlem1  6135  tfrlemi1  6159  tfr1onlemaccex  6175  tfrcllemaccex  6188  frecrdg  6235  oawordriexmid  6296  nnacl  6306  nnmcl  6307  nnacom  6310  nnaass  6311  nnmsucr  6314  nndifsnid  6333  nnmordi  6342  iinerm  6431  th3qlem2  6462  elpmg  6488  pmss12g  6499  mapsn  6514  brdomg  6572  f1domg  6582  ssdomg  6602  nndomo  6687  carden2bex  6956  addclpi  7036  addnidpig  7045  genpassl  7233  genpassu  7234  nqprloc  7254  ltaprlem  7327  recexprlemopl  7334  recexprlemopu  7336  recexprlemupu  7337  recexprlemss1l  7344  recexprlemss1u  7345  cauappcvgprlemupu  7358  caucvgprlemupu  7381  caucvgprprlemupu  7409  archsr  7477  peano2nnnn  7540  receuap  8291  peano2nn  8590  nnaddcl  8598  zrevaddcl  8956  nzadd  8958  zdiv  8991  nneo  9006  zeo2  9009  peano5uzti  9011  fzind  9018  fnn0ind  9019  lbzbi  9258  qrevaddcl  9286  irradd  9288  irrmul  9289  ltsubrp  9325  ltaddrp  9326  xnn0xadd0  9491  icoshft  9614  fzen  9664  elfzm11  9712  uzsplit  9713  fzoval  9766  elfzom1elp1fzo  9820  exfzdc  9858  modaddmodup  10001  frec2uzrdg  10023  seq3clss  10081  monoord  10090  seq3caopr3  10095  seq3f1olemp  10116  seq3id3  10121  seq3homo  10124  seq3z  10125  ser3ge0  10131  expadd  10176  expmul  10179  leexp1a  10189  faccl  10322  facdiv  10325  faclbnd  10328  faclbnd6  10331  omgadd  10389  hashunsng  10394  seq3coll  10426  shftlem  10429  resqrexlemover  10622  resqrexlemdecn  10624  resqrexlemlo  10625  resqrexlemcalc3  10628  climub  10952  climserle  10953  fsumzcl2  11013  fsumsplitsnun  11027  fsum2d  11043  modfsummodlemstep  11065  fsumabs  11073  fsumiun  11085  bcxmas  11097  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  dvds2ln  11321  dvdsabseq  11340  dvdsdivcl  11343  alzdvds  11347  oddnn02np1  11372  m1exp1  11393  nn0o1gt2  11397  nno  11398  ndvdsadd  11423  flodddiv4  11426  gcddiv  11500  gcdmultiple  11501  gcdmultiplez  11502  rplpwr  11508  dvdssq  11512  nn0seqcvgd  11515  alginv  11521  algcvga  11525  algfx  11526  isprm2  11591  isprm3  11592  prmdvdsexp  11619  ennnfoneleminc  11716  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemhom  11720  setsn0fun  11778  restopnb  12132  restdis  12135  tgcnp  12159  cnntr  12175  cnsscnp  12179  txcn  12225  txlm  12229  mettri  12301  blssexps  12357  blssex  12358  mopni3  12412  metss  12422  2spim  12555