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  903  dedlema  969  dedlemb  970  19.35-1  1624  cbval2  1921  cbvex2  1922  nelelne  2439  r19.21be  2568  r19.35-1  2627  mosubt  2915  sbcrext  3041  uneqdifeqim  3509  ssuni  3832  uniss2  3841  elpwuni  3977  elssabg  4149  elpw2g  4157  epelg  4291  elomssom  4605  relop  4778  riinint  4889  cnviinm  5171  funopg  5251  fun  5389  tz6.12c  5546  fvelrnb  5564  fmptco  5683  fnressn  5703  fressnfv  5704  fvtp2g  5726  fvtp3g  5727  fconst2g  5732  isores3  5816  isoselem  5821  eloprabga  5962  fo1stresm  6162  poxp  6233  brtpos2  6252  smores  6293  tfrlem1  6309  tfrlemi1  6333  tfr1onlemaccex  6349  tfrcllemaccex  6362  frecrdg  6409  oawordriexmid  6471  nnacl  6481  nnmcl  6482  nnacom  6485  nnaass  6486  nnmsucr  6489  nndifsnid  6508  nnmordi  6517  iinerm  6607  th3qlem2  6638  elpmg  6664  pmss12g  6675  mapsn  6690  brdomg  6748  f1domg  6758  ssdomg  6778  nndomo  6864  elfi2  6971  nnnninfeq2  7127  carden2bex  7188  cc3  7267  addclpi  7326  addnidpig  7335  genpassl  7523  genpassu  7524  nqprloc  7544  ltaprlem  7617  recexprlemopl  7624  recexprlemopu  7626  recexprlemupu  7627  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemupu  7648  caucvgprlemupu  7671  caucvgprprlemupu  7699  archsr  7781  peano2nnnn  7852  receuap  8626  peano2nn  8931  nnaddcl  8939  zrevaddcl  9303  nzadd  9305  zdiv  9341  nneo  9356  zeo2  9359  peano5uzti  9361  fzind  9368  fnn0ind  9369  lbzbi  9616  qrevaddcl  9644  irradd  9646  irrmul  9647  ltsubrp  9690  ltaddrp  9691  xnn0xadd0  9867  icoshft  9990  fzen  10043  elfzm11  10091  uzsplit  10092  fzoval  10148  elfzom1elp1fzo  10202  exfzdc  10240  modaddmodup  10387  frec2uzrdg  10409  seq3clss  10467  monoord  10476  seq3caopr3  10481  seq3f1olemp  10502  seq3id3  10507  seq3homo  10510  seq3z  10511  ser3ge0  10517  expadd  10562  expmul  10565  leexp1a  10575  modqexp  10647  faccl  10715  facdiv  10718  faclbnd  10721  faclbnd6  10724  omgadd  10782  hashunsng  10787  seq3coll  10822  shftlem  10825  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc3  11025  climub  11352  climserle  11353  fsumzcl2  11413  fsumsplitsnun  11427  fsum2d  11443  modfsummodlemstep  11465  fsumabs  11473  fsumiun  11485  bcxmas  11497  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  prodfap0  11553  prodfrecap  11554  ntrivcvgap  11556  prodmodc  11586  fprodssdc  11598  fprodabs  11624  fprod2d  11631  dvdsmod0  11800  dvds2ln  11831  dvdsabseq  11853  dvdsdivcl  11856  alzdvds  11860  oddnn02np1  11885  m1exp1  11906  nn0o1gt2  11910  nno  11911  ndvdsadd  11936  flodddiv4  11939  gcddiv  12020  gcdmultiple  12021  gcdmultiplez  12022  rplpwr  12028  dvdssq  12032  nn0seqcvgd  12041  alginv  12047  algcvga  12051  algfx  12052  isprm2  12117  isprm3  12118  prmdvdsexp  12148  eulerthlemrprm  12229  eulerthlema  12230  pcmpt  12341  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  omiunct  12445  nninfdclemlt  12452  setsn0fun  12499  mgmcl  12778  dfgrp3mlem  12968  mhmmulg  13024  srgpcomp  13173  lmodfopnelem1  13414  rmodislmodlem  13440  cnfldmulg  13473  cnfldexp  13474  restopnb  13684  restdis  13687  tgcnp  13712  cnntr  13728  cnsscnp  13732  txcn  13778  txlm  13782  mettri  13876  blssexps  13932  blssex  13933  mopni3  13987  metss  13997  2spim  14521