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  5829  fnressn  5839  fressnfv  5840  fvtp2g  5862  fvtp3g  5863  fconst2g  5868  isores3  5955  isoselem  5960  eloprabga  6107  fo1stresm  6323  poxp  6396  brtpos2  6416  smores  6457  tfrlem1  6473  tfrlemi1  6497  tfr1onlemaccex  6513  tfrcllemaccex  6526  frecrdg  6573  oawordriexmid  6637  nnacl  6647  nnmcl  6648  nnacom  6651  nnaass  6652  nnmsucr  6655  nndifsnid  6674  nnmordi  6683  iinerm  6775  th3qlem2  6806  elpmg  6832  pmss12g  6843  mapsn  6858  brdomg  6918  f1domg  6930  ssdomg  6951  nndomo  7049  elfi2  7170  nnnninfeq2  7327  carden2bex  7393  cc3  7486  addclpi  7546  addnidpig  7555  genpassl  7743  genpassu  7744  nqprloc  7764  ltaprlem  7837  recexprlemopl  7844  recexprlemopu  7846  recexprlemupu  7847  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemupu  7868  caucvgprlemupu  7891  caucvgprprlemupu  7919  archsr  8001  peano2nnnn  8072  receuap  8848  peano2nn  9154  nnaddcl  9162  zrevaddcl  9529  nzadd  9531  zdiv  9567  nneo  9582  zeo2  9585  peano5uzti  9587  fzind  9594  fnn0ind  9595  lbzbi  9849  qrevaddcl  9877  irradd  9879  irrmul  9880  ltsubrp  9924  ltaddrp  9925  xnn0xadd0  10101  icoshft  10224  fzen  10277  elfzm11  10325  uzsplit  10326  fzoval  10382  elfzom1elp1fzo  10446  exfzdc  10485  modaddmodup  10648  frec2uzrdg  10670  nninfinf  10704  seq3clss  10732  monoord  10746  seq3caopr3  10752  seqcaopr3g  10753  seq3f1olemp  10776  seqf1oglem2a  10779  seqf1og  10782  seq3id3  10785  seq3homo  10788  seq3z  10789  seqfeq4g  10792  ser3ge0  10797  expadd  10842  expmul  10845  leexp1a  10855  modqexp  10927  faccl  10996  facdiv  10999  faclbnd  11002  faclbnd6  11005  omgadd  11064  hashunsng  11070  seq3coll  11105  fundm2domnop0  11108  swrdswrdlem  11284  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccat3  11314  shftlem  11376  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc3  11576  climub  11904  climserle  11905  fsumzcl2  11965  fsumsplitsnun  11979  fsum2d  11995  modfsummodlemstep  12017  fsumabs  12025  fsumiun  12037  bcxmas  12049  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  prodfap0  12105  prodfrecap  12106  ntrivcvgap  12108  prodmodc  12138  fprodssdc  12150  fprodabs  12176  fprod2d  12183  dvdsmod0  12353  dvds2ln  12384  dvdsabseq  12407  dvdsdivcl  12410  alzdvds  12414  oddnn02np1  12440  m1exp1  12461  nn0o1gt2  12465  nno  12466  ndvdsadd  12491  flodddiv4  12496  bitsinv1  12522  gcddiv  12589  gcdmultiple  12590  gcdmultiplez  12591  rplpwr  12597  dvdssq  12601  nninfct  12611  nn0seqcvgd  12612  alginv  12618  algcvga  12622  algfx  12623  isprm2  12688  isprm3  12689  prmdvdsexp  12719  eulerthlemrprm  12800  eulerthlema  12801  pcmpt  12915  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemhom  13035  omiunct  13064  nninfdclemlt  13071  setsn0fun  13118  mgmcl  13441  dfgrp3mlem  13680  mhmmulg  13749  resghm2b  13848  gsumfzconst  13927  srgpcomp  14002  lmodfopnelem1  14337  rmodislmodlem  14363  lss1d  14396  cnfldmulg  14589  cnfldexp  14590  gsumfzfsumlemm  14600  restopnb  14904  restdis  14907  tgcnp  14932  cnntr  14948  cnsscnp  14952  txcn  14998  txlm  15002  mettri  15096  blssexps  15152  blssex  15153  mopni3  15207  metss  15217  dvmptfsum  15448  plycolemc  15481  rpcxpmul2  15636  gausslemma2dlem6  15795  lgsquad2lem2  15810  2lgslem1c  15818  2lgslem3  15829  2lgs  15832  uhgredgrnv  15988  usgruspgrben  16036  usgredg2vlem2  16073  subupgr  16123  uspgr2wlkeq  16215  clwwlkccatlem  16250  umgrclwwlkge2  16252  clwwlkn1loopb  16270  clwwlknonex2lem2  16288  2spim  16362