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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  565  pm4.79dc  915  dedlema  982  dedlemb  983  19.35-1  1677  cbval2  1977  cbvex2  1978  nelelne  2512  r19.21be  2641  r19.35-1  2701  mosubt  3003  sbcrext  3129  uneqdifeqim  3613  ssuni  3957  uniss2  3966  elpwuni  4102  elssabg  4286  elpw2g  4294  epelg  4437  elomssom  4754  relop  4932  riinint  5045  cnviinm  5332  funopg  5414  fun  5564  tz6.12c  5728  fvelrnb  5753  fmptco  5877  funopsn  5894  fnressn  5904  fressnfv  5905  fvtp2g  5927  fvtp3g  5928  fconst2g  5933  isores3  6024  isoselem  6029  eloprabga  6178  fo1stresm  6399  poxp  6472  fsuppeq  6491  suppssdc  6504  brtpos2  6527  smores  6568  tfrlem1  6584  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  frecrdg  6684  oawordriexmid  6748  nnacl  6758  nnmcl  6759  nnacom  6762  nnaass  6763  nnmsucr  6766  nndifsnid  6785  nnmordi  6794  iinerm  6886  th3qlem2  6917  elpmg  6943  pmss12g  6961  mapsn  6978  brdomg  7038  f1domg  7050  ssdomg  7071  nndomo  7171  elfi2  7311  nnnninfeq2  7475  carden2bex  7541  cc3  7640  addclpi  7700  addnidpig  7709  genpassl  7897  genpassu  7898  nqprloc  7918  ltaprlem  7991  recexprlemopl  7998  recexprlemopu  8000  recexprlemupu  8001  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemupu  8022  caucvgprlemupu  8045  caucvgprprlemupu  8073  archsr  8155  peano2nnnn  8226  receuap  9007  indval0  9306  peano2nn  9325  nnaddcl  9333  zrevaddcl  9704  nzadd  9706  zdiv  9744  nneo  9759  zeo2  9762  peano5uzti  9764  fzind  9771  fnn0ind  9772  lbzbi  10031  qrevaddcl  10059  irradd  10061  irrmul  10063  ltsubrp  10107  ltaddrp  10108  xnn0xadd0  10285  icoshft  10408  fzen  10463  elfzm11  10514  uzsplit  10515  fzoval  10571  elfzom1elp1fzo  10636  exfzdc  10675  modaddmodup  10844  frec2uzrdg  10866  nninfinf  10900  seq3clss  10928  monoord  10942  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemp  10972  seqf1oglem2a  10975  seqf1og  10978  seq3id3  10981  seq3homo  10984  seq3z  10985  seqfeq4g  10988  ser3ge0  10993  expadd  11038  expmul  11041  leexp1a  11051  modqexp  11124  faccl  11194  facdiv  11197  faclbnd  11200  faclbnd6  11203  omgadd  11263  hashunsng  11269  hashmap  11289  hashf1  11308  seq3coll  11315  fundm2domnop0  11321  swrdswrdlem  11497  swrdswrd  11498  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccat3  11527  shftlem  11602  resqrexlemover  11797  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc3  11803  climub  12134  climserle  12135  fsumzcl2  12196  fsumsplitsnun  12210  fsum2d  12226  modfsummodlemstep  12248  fsumabs  12256  fsumiun  12268  bcxmas  12280  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  prodfap0  12336  prodfrecap  12337  ntrivcvgap  12339  prodmodc  12369  fprodssdc  12381  fprodabs  12407  fprod2d  12414  dvdsmod0  12584  dvds2ln  12615  dvdsabseq  12638  dvdsdivcl  12641  alzdvds  12645  oddnn02np1  12671  m1exp1  12692  nn0o1gt2  12696  nno  12697  ndvdsadd  12722  flodddiv4  12727  bitsinv1  12753  gcddiv  12820  gcdmultiple  12821  gcdmultiplez  12822  rplpwr  12828  dvdssq  12832  nninfct  12842  nn0seqcvgd  12843  alginv  12849  algcvga  12853  algfx  12854  isprm2  12919  isprm3  12920  prmdvdsexp  12951  eulerthlemrprm  13035  eulerthlema  13036  pcmpt  13150  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemhom  13363  omiunct  13392  nninfdclemlt  13399  setsn0fun  13446  mgmcl  13737  dfgrp3mlem  13961  mhmmulg  14024  resghm2b  14123  cntzval  14152  gzsumconst  14232  srgpcomp  14400  lmodfopnelem1  14769  rmodislmodlem  14795  lss1d  14828  cnfldmulg  15021  cnfldexp  15022  restopnb  15424  restdis  15427  tgcnp  15452  cnntr  15468  cnsscnp  15472  txcn  15518  txlm  15522  mettri  15616  blssexps  15672  blssex  15673  mopni3  15727  metss  15737  dvmptfsum  15968  plycolemc  16001  rpcxpmul2  16163  ppiqub  16310  bcmono  16321  bpos1lem  16326  bposlem5  16332  gausslemma2dlem6  16408  lgsquad2lem2  16423  2lgslem1c  16431  2lgslem3  16442  2lgs  16445  uhgredgrnv  16601  usgruspgrben  16649  usgredg2vlem2  16686  subupgr  16736  uspgr2wlkeq  16828  clwwlkccatlem  16863  umgrclwwlkge2  16865  clwwlkn1loopb  16883  clwwlknonex2lem2  16901  eupth2lem3lem4fi  16936  eupth2fi  16942  2spim  17016  exmidcon  17259  alsralrex  17377