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  904  dedlema  971  dedlemb  972  19.35-1  1638  cbval2  1936  cbvex2  1937  nelelne  2459  r19.21be  2588  r19.35-1  2647  mosubt  2941  sbcrext  3067  uneqdifeqim  3537  ssuni  3862  uniss2  3871  elpwuni  4007  elssabg  4182  elpw2g  4190  epelg  4326  elomssom  4642  relop  4817  riinint  4928  cnviinm  5212  funopg  5293  fun  5433  tz6.12c  5591  fvelrnb  5611  fmptco  5731  fnressn  5751  fressnfv  5752  fvtp2g  5774  fvtp3g  5775  fconst2g  5780  isores3  5865  isoselem  5870  eloprabga  6013  fo1stresm  6228  poxp  6299  brtpos2  6318  smores  6359  tfrlem1  6375  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  frecrdg  6475  oawordriexmid  6537  nnacl  6547  nnmcl  6548  nnacom  6551  nnaass  6552  nnmsucr  6555  nndifsnid  6574  nnmordi  6583  iinerm  6675  th3qlem2  6706  elpmg  6732  pmss12g  6743  mapsn  6758  brdomg  6816  f1domg  6826  ssdomg  6846  nndomo  6934  elfi2  7047  nnnninfeq2  7204  carden2bex  7268  cc3  7351  addclpi  7411  addnidpig  7420  genpassl  7608  genpassu  7609  nqprloc  7629  ltaprlem  7702  recexprlemopl  7709  recexprlemopu  7711  recexprlemupu  7712  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemupu  7733  caucvgprlemupu  7756  caucvgprprlemupu  7784  archsr  7866  peano2nnnn  7937  receuap  8713  peano2nn  9019  nnaddcl  9027  zrevaddcl  9393  nzadd  9395  zdiv  9431  nneo  9446  zeo2  9449  peano5uzti  9451  fzind  9458  fnn0ind  9459  lbzbi  9707  qrevaddcl  9735  irradd  9737  irrmul  9738  ltsubrp  9782  ltaddrp  9783  xnn0xadd0  9959  icoshft  10082  fzen  10135  elfzm11  10183  uzsplit  10184  fzoval  10240  elfzom1elp1fzo  10295  exfzdc  10333  modaddmodup  10496  frec2uzrdg  10518  nninfinf  10552  seq3clss  10580  monoord  10594  seq3caopr3  10600  seqcaopr3g  10601  seq3f1olemp  10624  seqf1oglem2a  10627  seqf1og  10630  seq3id3  10633  seq3homo  10636  seq3z  10637  seqfeq4g  10640  ser3ge0  10645  expadd  10690  expmul  10693  leexp1a  10703  modqexp  10775  faccl  10844  facdiv  10847  faclbnd  10850  faclbnd6  10853  omgadd  10911  hashunsng  10916  seq3coll  10951  shftlem  10998  resqrexlemover  11192  resqrexlemdecn  11194  resqrexlemlo  11195  resqrexlemcalc3  11198  climub  11526  climserle  11527  fsumzcl2  11587  fsumsplitsnun  11601  fsum2d  11617  modfsummodlemstep  11639  fsumabs  11647  fsumiun  11659  bcxmas  11671  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  prodfap0  11727  prodfrecap  11728  ntrivcvgap  11730  prodmodc  11760  fprodssdc  11772  fprodabs  11798  fprod2d  11805  dvdsmod0  11975  dvds2ln  12006  dvdsabseq  12029  dvdsdivcl  12032  alzdvds  12036  oddnn02np1  12062  m1exp1  12083  nn0o1gt2  12087  nno  12088  ndvdsadd  12113  flodddiv4  12118  bitsinv1  12144  gcddiv  12211  gcdmultiple  12212  gcdmultiplez  12213  rplpwr  12219  dvdssq  12223  nninfct  12233  nn0seqcvgd  12234  alginv  12240  algcvga  12244  algfx  12245  isprm2  12310  isprm3  12311  prmdvdsexp  12341  eulerthlemrprm  12422  eulerthlema  12423  pcmpt  12537  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemhom  12657  omiunct  12686  nninfdclemlt  12693  setsn0fun  12740  mgmcl  13061  dfgrp3mlem  13300  mhmmulg  13369  resghm2b  13468  gsumfzconst  13547  srgpcomp  13622  lmodfopnelem1  13956  rmodislmodlem  13982  lss1d  14015  cnfldmulg  14208  cnfldexp  14209  gsumfzfsumlemm  14219  restopnb  14501  restdis  14504  tgcnp  14529  cnntr  14545  cnsscnp  14549  txcn  14595  txlm  14599  mettri  14693  blssexps  14749  blssex  14750  mopni3  14804  metss  14814  dvmptfsum  15045  plycolemc  15078  rpcxpmul2  15233  gausslemma2dlem6  15392  lgsquad2lem2  15407  2lgslem1c  15415  2lgslem3  15426  2lgs  15429  2spim  15496