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  6526  smores  6567  tfrlem1  6583  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  frecrdg  6683  oawordriexmid  6747  nnacl  6757  nnmcl  6758  nnacom  6761  nnaass  6762  nnmsucr  6765  nndifsnid  6784  nnmordi  6793  iinerm  6885  th3qlem2  6916  elpmg  6942  pmss12g  6960  mapsn  6976  brdomg  7036  f1domg  7048  ssdomg  7069  nndomo  7169  ffsuppbi  7305  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  9706  nzadd  9708  zdiv  9745  nneo  9760  zeo2  9763  peano5uzti  9765  fzind  9772  fnn0ind  9773  lbzbi  10032  qrevaddcl  10060  irradd  10062  irrmul  10064  ltsubrp  10108  ltaddrp  10109  xnn0xadd0  10286  icoshft  10409  fzen  10464  elfzm11  10515  uzsplit  10516  fzoval  10572  elfzom1elp1fzo  10637  exfzdc  10676  modaddmodup  10845  frec2uzrdg  10867  nninfinf  10901  seq3clss  10929  monoord  10943  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemp  10973  seqf1oglem2a  10976  seqf1og  10979  seq3id3  10982  seq3homo  10985  seq3z  10986  seqfeq4g  10989  ser3ge0  10994  expadd  11039  expmul  11042  leexp1a  11052  modqexp  11125  faccl  11195  facdiv  11198  faclbnd  11201  faclbnd6  11204  omgadd  11264  hashunsng  11270  hashmap  11290  hashf1  11309  seq3coll  11316  fundm2domnop0  11322  swrdswrdlem  11498  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccat3  11528  shftlem  11603  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc3  11804  climub  12135  climserle  12136  fsumzcl2  12197  fsumsplitsnun  12211  fsum2d  12227  modfsummodlemstep  12249  fsumabs  12257  fsumiun  12269  bcxmas  12281  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  prodfap0  12337  prodfrecap  12338  ntrivcvgap  12340  prodmodc  12370  fprodssdc  12382  fprodabs  12408  fprod2d  12415  dvdsmod0  12585  dvds2ln  12616  dvdsabseq  12639  dvdsdivcl  12642  alzdvds  12646  oddnn02np1  12672  m1exp1  12693  nn0o1gt2  12697  nno  12698  ndvdsadd  12723  flodddiv4  12728  bitsinv1  12754  gcddiv  12821  gcdmultiple  12822  gcdmultiplez  12823  rplpwr  12829  dvdssq  12833  nninfct  12843  nn0seqcvgd  12844  alginv  12850  algcvga  12854  algfx  12855  isprm2  12920  isprm3  12921  prmdvdsexp  12952  eulerthlemrprm  13036  eulerthlema  13037  pcmpt  13151  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  omiunct  13393  nninfdclemlt  13400  setsn0fun  13447  mgmcl  13738  dfgrp3mlem  13962  mhmmulg  14025  resghm2b  14124  cntzval  14153  gzsumconst  14233  srgpcomp  14401  lmodfopnelem1  14770  rmodislmodlem  14796  lss1d  14829  cnfldmulg  15022  cnfldexp  15023  restopnb  15407  restdis  15410  tgcnp  15435  cnntr  15451  cnsscnp  15455  txcn  15501  txlm  15505  mettri  15599  blssexps  15655  blssex  15656  mopni3  15710  metss  15720  dvmptfsum  15951  plycolemc  15984  rpcxpmul2  16146  ppiqub  16293  bcmono  16304  bpos1lem  16309  bposlem5  16315  gausslemma2dlem6  16391  lgsquad2lem2  16406  2lgslem1c  16414  2lgslem3  16425  2lgs  16428  uhgredgrnv  16584  usgruspgrben  16632  usgredg2vlem2  16669  subupgr  16719  uspgr2wlkeq  16811  clwwlkccatlem  16846  umgrclwwlkge2  16848  clwwlkn1loopb  16866  clwwlknonex2lem2  16884  eupth2lem3lem4fi  16919  eupth2fi  16925  2spim  16999  exmidcon  17242  alsralrex  17360