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  1646  cbval2  1944  cbvex2  1945  nelelne  2467  r19.21be  2596  r19.35-1  2655  mosubt  2949  sbcrext  3075  uneqdifeqim  3545  ssuni  3871  uniss2  3880  elpwuni  4016  elssabg  4191  elpw2g  4199  epelg  4336  elomssom  4652  relop  4827  riinint  4938  cnviinm  5223  funopg  5304  fun  5447  tz6.12c  5605  fvelrnb  5625  fmptco  5745  funopsn  5761  fnressn  5769  fressnfv  5770  fvtp2g  5792  fvtp3g  5793  fconst2g  5798  isores3  5883  isoselem  5888  eloprabga  6031  fo1stresm  6246  poxp  6317  brtpos2  6336  smores  6377  tfrlem1  6393  tfrlemi1  6417  tfr1onlemaccex  6433  tfrcllemaccex  6446  frecrdg  6493  oawordriexmid  6555  nnacl  6565  nnmcl  6566  nnacom  6569  nnaass  6570  nnmsucr  6573  nndifsnid  6592  nnmordi  6601  iinerm  6693  th3qlem2  6724  elpmg  6750  pmss12g  6761  mapsn  6776  brdomg  6836  f1domg  6848  ssdomg  6869  nndomo  6960  elfi2  7073  nnnninfeq2  7230  carden2bex  7296  cc3  7379  addclpi  7439  addnidpig  7448  genpassl  7636  genpassu  7637  nqprloc  7657  ltaprlem  7730  recexprlemopl  7737  recexprlemopu  7739  recexprlemupu  7740  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemupu  7761  caucvgprlemupu  7784  caucvgprprlemupu  7812  archsr  7894  peano2nnnn  7965  receuap  8741  peano2nn  9047  nnaddcl  9055  zrevaddcl  9422  nzadd  9424  zdiv  9460  nneo  9475  zeo2  9478  peano5uzti  9480  fzind  9487  fnn0ind  9488  lbzbi  9736  qrevaddcl  9764  irradd  9766  irrmul  9767  ltsubrp  9811  ltaddrp  9812  xnn0xadd0  9988  icoshft  10111  fzen  10164  elfzm11  10212  uzsplit  10213  fzoval  10269  elfzom1elp1fzo  10329  exfzdc  10367  modaddmodup  10530  frec2uzrdg  10552  nninfinf  10586  seq3clss  10614  monoord  10628  seq3caopr3  10634  seqcaopr3g  10635  seq3f1olemp  10658  seqf1oglem2a  10661  seqf1og  10664  seq3id3  10667  seq3homo  10670  seq3z  10671  seqfeq4g  10674  ser3ge0  10679  expadd  10724  expmul  10727  leexp1a  10737  modqexp  10809  faccl  10878  facdiv  10881  faclbnd  10884  faclbnd6  10887  omgadd  10945  hashunsng  10950  seq3coll  10985  fundm2domnop0  10988  shftlem  11098  resqrexlemover  11292  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc3  11298  climub  11626  climserle  11627  fsumzcl2  11687  fsumsplitsnun  11701  fsum2d  11717  modfsummodlemstep  11739  fsumabs  11747  fsumiun  11759  bcxmas  11771  cvgratnnlemnexp  11806  cvgratnnlemmn  11807  prodfap0  11827  prodfrecap  11828  ntrivcvgap  11830  prodmodc  11860  fprodssdc  11872  fprodabs  11898  fprod2d  11905  dvdsmod0  12075  dvds2ln  12106  dvdsabseq  12129  dvdsdivcl  12132  alzdvds  12136  oddnn02np1  12162  m1exp1  12183  nn0o1gt2  12187  nno  12188  ndvdsadd  12213  flodddiv4  12218  bitsinv1  12244  gcddiv  12311  gcdmultiple  12312  gcdmultiplez  12313  rplpwr  12319  dvdssq  12323  nninfct  12333  nn0seqcvgd  12334  alginv  12340  algcvga  12344  algfx  12345  isprm2  12410  isprm3  12411  prmdvdsexp  12441  eulerthlemrprm  12522  eulerthlema  12523  pcmpt  12637  ennnfoneleminc  12753  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemhom  12757  omiunct  12786  nninfdclemlt  12793  setsn0fun  12840  mgmcl  13162  dfgrp3mlem  13401  mhmmulg  13470  resghm2b  13569  gsumfzconst  13648  srgpcomp  13723  lmodfopnelem1  14057  rmodislmodlem  14083  lss1d  14116  cnfldmulg  14309  cnfldexp  14310  gsumfzfsumlemm  14320  restopnb  14624  restdis  14627  tgcnp  14652  cnntr  14668  cnsscnp  14672  txcn  14718  txlm  14722  mettri  14816  blssexps  14872  blssex  14873  mopni3  14927  metss  14937  dvmptfsum  15168  plycolemc  15201  rpcxpmul2  15356  gausslemma2dlem6  15515  lgsquad2lem2  15530  2lgslem1c  15538  2lgslem3  15549  2lgs  15552  2spim  15664