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  561  pm4.79dc  910  dedlema  977  dedlemb  978  19.35-1  1672  cbval2  1970  cbvex2  1971  nelelne  2494  r19.21be  2623  r19.35-1  2683  mosubt  2983  sbcrext  3109  uneqdifeqim  3580  ssuni  3915  uniss2  3924  elpwuni  4060  elssabg  4238  elpw2g  4246  epelg  4387  elomssom  4703  relop  4880  riinint  4993  cnviinm  5278  funopg  5360  fun  5508  tz6.12c  5669  fvelrnb  5693  fmptco  5813  funopsn  5830  fnressn  5840  fressnfv  5841  fvtp2g  5863  fvtp3g  5864  fconst2g  5869  isores3  5956  isoselem  5961  eloprabga  6108  fo1stresm  6324  poxp  6397  brtpos2  6417  smores  6458  tfrlem1  6474  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  frecrdg  6574  oawordriexmid  6638  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nnmsucr  6656  nndifsnid  6675  nnmordi  6684  iinerm  6776  th3qlem2  6807  elpmg  6833  pmss12g  6844  mapsn  6859  brdomg  6919  f1domg  6931  ssdomg  6952  nndomo  7050  elfi2  7171  nnnninfeq2  7328  carden2bex  7394  cc3  7487  addclpi  7547  addnidpig  7556  genpassl  7744  genpassu  7745  nqprloc  7765  ltaprlem  7838  recexprlemopl  7845  recexprlemopu  7847  recexprlemupu  7848  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemupu  7869  caucvgprlemupu  7892  caucvgprprlemupu  7920  archsr  8002  peano2nnnn  8073  receuap  8849  peano2nn  9155  nnaddcl  9163  zrevaddcl  9530  nzadd  9532  zdiv  9568  nneo  9583  zeo2  9586  peano5uzti  9588  fzind  9595  fnn0ind  9596  lbzbi  9850  qrevaddcl  9878  irradd  9880  irrmul  9881  ltsubrp  9925  ltaddrp  9926  xnn0xadd0  10102  icoshft  10225  fzen  10278  elfzm11  10326  uzsplit  10327  fzoval  10383  elfzom1elp1fzo  10448  exfzdc  10487  modaddmodup  10650  frec2uzrdg  10672  nninfinf  10706  seq3clss  10734  monoord  10748  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3homo  10790  seq3z  10791  seqfeq4g  10794  ser3ge0  10799  expadd  10844  expmul  10847  leexp1a  10857  modqexp  10929  faccl  10998  facdiv  11001  faclbnd  11004  faclbnd6  11007  omgadd  11066  hashunsng  11072  seq3coll  11107  fundm2domnop0  11113  swrdswrdlem  11289  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccat3  11319  shftlem  11381  resqrexlemover  11575  resqrexlemdecn  11577  resqrexlemlo  11578  resqrexlemcalc3  11581  climub  11909  climserle  11910  fsumzcl2  11971  fsumsplitsnun  11985  fsum2d  12001  modfsummodlemstep  12023  fsumabs  12031  fsumiun  12043  bcxmas  12055  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  prodfap0  12111  prodfrecap  12112  ntrivcvgap  12114  prodmodc  12144  fprodssdc  12156  fprodabs  12182  fprod2d  12189  dvdsmod0  12359  dvds2ln  12390  dvdsabseq  12413  dvdsdivcl  12416  alzdvds  12420  oddnn02np1  12446  m1exp1  12467  nn0o1gt2  12471  nno  12472  ndvdsadd  12497  flodddiv4  12502  bitsinv1  12528  gcddiv  12595  gcdmultiple  12596  gcdmultiplez  12597  rplpwr  12603  dvdssq  12607  nninfct  12617  nn0seqcvgd  12618  alginv  12624  algcvga  12628  algfx  12629  isprm2  12694  isprm3  12695  prmdvdsexp  12725  eulerthlemrprm  12806  eulerthlema  12807  pcmpt  12921  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemhom  13041  omiunct  13070  nninfdclemlt  13077  setsn0fun  13124  mgmcl  13447  dfgrp3mlem  13686  mhmmulg  13755  resghm2b  13854  gsumfzconst  13933  srgpcomp  14009  lmodfopnelem1  14344  rmodislmodlem  14370  lss1d  14403  cnfldmulg  14596  cnfldexp  14597  gsumfzfsumlemm  14607  restopnb  14911  restdis  14914  tgcnp  14939  cnntr  14955  cnsscnp  14959  txcn  15005  txlm  15009  mettri  15103  blssexps  15159  blssex  15160  mopni3  15214  metss  15224  dvmptfsum  15455  plycolemc  15488  rpcxpmul2  15643  gausslemma2dlem6  15802  lgsquad2lem2  15817  2lgslem1c  15825  2lgslem3  15836  2lgs  15839  uhgredgrnv  15995  usgruspgrben  16043  usgredg2vlem2  16080  subupgr  16130  uspgr2wlkeq  16222  clwwlkccatlem  16257  umgrclwwlkge2  16259  clwwlkn1loopb  16277  clwwlknonex2lem2  16295  eupth2lem3lem4fi  16330  eupth2fi  16336  2spim  16388