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  2981  sbcrext  3107  uneqdifeqim  3578  ssuni  3913  uniss2  3922  elpwuni  4058  elssabg  4236  elpw2g  4244  epelg  4385  elomssom  4701  relop  4878  riinint  4991  cnviinm  5276  funopg  5358  fun  5505  tz6.12c  5665  fvelrnb  5689  fmptco  5809  funopsn  5825  fnressn  5835  fressnfv  5836  fvtp2g  5858  fvtp3g  5859  fconst2g  5864  isores3  5951  isoselem  5956  eloprabga  6103  fo1stresm  6319  poxp  6392  brtpos2  6412  smores  6453  tfrlem1  6469  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  frecrdg  6569  oawordriexmid  6633  nnacl  6643  nnmcl  6644  nnacom  6647  nnaass  6648  nnmsucr  6651  nndifsnid  6670  nnmordi  6679  iinerm  6771  th3qlem2  6802  elpmg  6828  pmss12g  6839  mapsn  6854  brdomg  6914  f1domg  6926  ssdomg  6947  nndomo  7045  elfi2  7162  nnnninfeq2  7319  carden2bex  7385  cc3  7477  addclpi  7537  addnidpig  7546  genpassl  7734  genpassu  7735  nqprloc  7755  ltaprlem  7828  recexprlemopl  7835  recexprlemopu  7837  recexprlemupu  7838  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemupu  7859  caucvgprlemupu  7882  caucvgprprlemupu  7910  archsr  7992  peano2nnnn  8063  receuap  8839  peano2nn  9145  nnaddcl  9153  zrevaddcl  9520  nzadd  9522  zdiv  9558  nneo  9573  zeo2  9576  peano5uzti  9578  fzind  9585  fnn0ind  9586  lbzbi  9840  qrevaddcl  9868  irradd  9870  irrmul  9871  ltsubrp  9915  ltaddrp  9916  xnn0xadd0  10092  icoshft  10215  fzen  10268  elfzm11  10316  uzsplit  10317  fzoval  10373  elfzom1elp1fzo  10437  exfzdc  10476  modaddmodup  10639  frec2uzrdg  10661  nninfinf  10695  seq3clss  10723  monoord  10737  seq3caopr3  10743  seqcaopr3g  10744  seq3f1olemp  10767  seqf1oglem2a  10770  seqf1og  10773  seq3id3  10776  seq3homo  10779  seq3z  10780  seqfeq4g  10783  ser3ge0  10788  expadd  10833  expmul  10836  leexp1a  10846  modqexp  10918  faccl  10987  facdiv  10990  faclbnd  10993  faclbnd6  10996  omgadd  11055  hashunsng  11061  seq3coll  11096  fundm2domnop0  11099  swrdswrdlem  11275  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccat3  11305  shftlem  11367  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc3  11567  climub  11895  climserle  11896  fsumzcl2  11956  fsumsplitsnun  11970  fsum2d  11986  modfsummodlemstep  12008  fsumabs  12016  fsumiun  12028  bcxmas  12040  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  prodfap0  12096  prodfrecap  12097  ntrivcvgap  12099  prodmodc  12129  fprodssdc  12141  fprodabs  12167  fprod2d  12174  dvdsmod0  12344  dvds2ln  12375  dvdsabseq  12398  dvdsdivcl  12401  alzdvds  12405  oddnn02np1  12431  m1exp1  12452  nn0o1gt2  12456  nno  12457  ndvdsadd  12482  flodddiv4  12487  bitsinv1  12513  gcddiv  12580  gcdmultiple  12581  gcdmultiplez  12582  rplpwr  12588  dvdssq  12592  nninfct  12602  nn0seqcvgd  12603  alginv  12609  algcvga  12613  algfx  12614  isprm2  12679  isprm3  12680  prmdvdsexp  12710  eulerthlemrprm  12791  eulerthlema  12792  pcmpt  12906  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemhom  13026  omiunct  13055  nninfdclemlt  13062  setsn0fun  13109  mgmcl  13432  dfgrp3mlem  13671  mhmmulg  13740  resghm2b  13839  gsumfzconst  13918  srgpcomp  13993  lmodfopnelem1  14328  rmodislmodlem  14354  lss1d  14387  cnfldmulg  14580  cnfldexp  14581  gsumfzfsumlemm  14591  restopnb  14895  restdis  14898  tgcnp  14923  cnntr  14939  cnsscnp  14943  txcn  14989  txlm  14993  mettri  15087  blssexps  15143  blssex  15144  mopni3  15198  metss  15208  dvmptfsum  15439  plycolemc  15472  rpcxpmul2  15627  gausslemma2dlem6  15786  lgsquad2lem2  15801  2lgslem1c  15809  2lgslem3  15820  2lgs  15823  uhgredgrnv  15977  usgruspgrben  16025  usgredg2vlem2  16062  uspgr2wlkeq  16162  clwwlkccatlem  16195  umgrclwwlkge2  16197  clwwlkn1loopb  16215  clwwlknonex2lem2  16233  2spim  16298