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  911  dedlema  978  dedlemb  979  19.35-1  1673  cbval2  1971  cbvex2  1972  nelelne  2504  r19.21be  2633  r19.35-1  2693  mosubt  2994  sbcrext  3120  uneqdifeqim  3595  ssuni  3936  uniss2  3945  elpwuni  4081  elssabg  4260  elpw2g  4268  epelg  4411  elomssom  4727  relop  4905  riinint  5018  cnviinm  5304  funopg  5386  fun  5536  tz6.12c  5700  fvelrnb  5724  fmptco  5843  funopsn  5860  fnressn  5870  fressnfv  5871  fvtp2g  5893  fvtp3g  5894  fconst2g  5899  isores3  5988  isoselem  5993  eloprabga  6140  fo1stresm  6355  poxp  6428  fsuppeq  6447  suppssdc  6460  brtpos2  6482  smores  6523  tfrlem1  6539  tfrlemi1  6563  tfr1onlemaccex  6579  tfrcllemaccex  6592  frecrdg  6639  oawordriexmid  6703  nnacl  6713  nnmcl  6714  nnacom  6717  nnaass  6718  nnmsucr  6721  nndifsnid  6740  nnmordi  6749  iinerm  6841  th3qlem2  6872  elpmg  6898  pmss12g  6909  mapsn  6925  brdomg  6985  f1domg  6997  ssdomg  7018  nndomo  7118  ffsuppbi  7253  elfi2  7259  nnnninfeq2  7420  carden2bex  7486  cc3  7582  addclpi  7642  addnidpig  7651  genpassl  7839  genpassu  7840  nqprloc  7860  ltaprlem  7933  recexprlemopl  7940  recexprlemopu  7942  recexprlemupu  7943  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemupu  7964  caucvgprlemupu  7987  caucvgprprlemupu  8015  archsr  8097  peano2nnnn  8168  receuap  8943  peano2nn  9249  nnaddcl  9257  zrevaddcl  9628  nzadd  9630  zdiv  9666  nneo  9681  zeo2  9684  peano5uzti  9686  fzind  9693  fnn0ind  9694  lbzbi  9948  qrevaddcl  9976  irradd  9978  irrmul  9979  ltsubrp  10023  ltaddrp  10024  xnn0xadd0  10200  icoshft  10323  fzen  10377  elfzm11  10425  uzsplit  10426  fzoval  10482  elfzom1elp1fzo  10547  exfzdc  10586  modaddmodup  10749  frec2uzrdg  10771  nninfinf  10805  seq3clss  10833  monoord  10847  seq3caopr3  10853  seqcaopr3g  10854  seq3f1olemp  10877  seqf1oglem2a  10880  seqf1og  10883  seq3id3  10886  seq3homo  10889  seq3z  10890  seqfeq4g  10893  ser3ge0  10898  expadd  10943  expmul  10946  leexp1a  10956  modqexp  11028  faccl  11097  facdiv  11100  faclbnd  11103  faclbnd6  11106  omgadd  11166  hashunsng  11172  hashmap  11192  seq3coll  11214  fundm2domnop0  11220  swrdswrdlem  11396  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccat3  11426  shftlem  11501  resqrexlemover  11695  resqrexlemdecn  11697  resqrexlemlo  11698  resqrexlemcalc3  11701  climub  12029  climserle  12030  fsumzcl2  12091  fsumsplitsnun  12105  fsum2d  12121  modfsummodlemstep  12143  fsumabs  12151  fsumiun  12163  bcxmas  12175  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  prodfap0  12231  prodfrecap  12232  ntrivcvgap  12234  prodmodc  12264  fprodssdc  12276  fprodabs  12302  fprod2d  12309  dvdsmod0  12479  dvds2ln  12510  dvdsabseq  12533  dvdsdivcl  12536  alzdvds  12540  oddnn02np1  12566  m1exp1  12587  nn0o1gt2  12591  nno  12592  ndvdsadd  12617  flodddiv4  12622  bitsinv1  12648  gcddiv  12715  gcdmultiple  12716  gcdmultiplez  12717  rplpwr  12723  dvdssq  12727  nninfct  12737  nn0seqcvgd  12738  alginv  12744  algcvga  12748  algfx  12749  isprm2  12814  isprm3  12815  prmdvdsexp  12845  eulerthlemrprm  12926  eulerthlema  12927  pcmpt  13041  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemhom  13166  omiunct  13195  nninfdclemlt  13202  setsn0fun  13249  mgmcl  13572  dfgrp3mlem  13811  mhmmulg  13880  resghm2b  13979  gsumfzconst  14058  srgpcomp  14134  lmodfopnelem1  14472  rmodislmodlem  14498  lss1d  14531  cnfldmulg  14724  cnfldexp  14725  gsumfzfsumlemm  14735  restopnb  15046  restdis  15049  tgcnp  15074  cnntr  15090  cnsscnp  15094  txcn  15140  txlm  15144  mettri  15238  blssexps  15294  blssex  15295  mopni3  15349  metss  15359  dvmptfsum  15590  plycolemc  15623  rpcxpmul2  15778  gausslemma2dlem6  15940  lgsquad2lem2  15955  2lgslem1c  15963  2lgslem3  15974  2lgs  15977  uhgredgrnv  16133  usgruspgrben  16181  usgredg2vlem2  16218  subupgr  16268  uspgr2wlkeq  16360  clwwlkccatlem  16395  umgrclwwlkge2  16397  clwwlkn1loopb  16415  clwwlknonex2lem2  16433  eupth2lem3lem4fi  16468  eupth2fi  16474  2spim  16538  exmidcon  16780