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  1970  cbvex2  1971  nelelne  2495  r19.21be  2624  r19.35-1  2684  mosubt  2984  sbcrext  3110  uneqdifeqim  3582  ssuni  3920  uniss2  3929  elpwuni  4065  elssabg  4243  elpw2g  4251  epelg  4393  elomssom  4709  relop  4886  riinint  4999  cnviinm  5285  funopg  5367  fun  5516  tz6.12c  5678  fvelrnb  5702  fmptco  5821  funopsn  5838  fnressn  5848  fressnfv  5849  fvtp2g  5871  fvtp3g  5872  fconst2g  5877  isores3  5966  isoselem  5971  eloprabga  6118  fo1stresm  6333  poxp  6406  fsuppeq  6425  suppssdc  6438  brtpos2  6460  smores  6501  tfrlem1  6517  tfrlemi1  6541  tfr1onlemaccex  6557  tfrcllemaccex  6570  frecrdg  6617  oawordriexmid  6681  nnacl  6691  nnmcl  6692  nnacom  6695  nnaass  6696  nnmsucr  6699  nndifsnid  6718  nnmordi  6727  iinerm  6819  th3qlem2  6850  elpmg  6876  pmss12g  6887  mapsn  6902  brdomg  6962  f1domg  6974  ssdomg  6995  nndomo  7093  elfi2  7214  nnnninfeq2  7371  carden2bex  7437  cc3  7530  addclpi  7590  addnidpig  7599  genpassl  7787  genpassu  7788  nqprloc  7808  ltaprlem  7881  recexprlemopl  7888  recexprlemopu  7890  recexprlemupu  7891  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemupu  7912  caucvgprlemupu  7935  caucvgprprlemupu  7963  archsr  8045  peano2nnnn  8116  receuap  8891  peano2nn  9197  nnaddcl  9205  zrevaddcl  9574  nzadd  9576  zdiv  9612  nneo  9627  zeo2  9630  peano5uzti  9632  fzind  9639  fnn0ind  9640  lbzbi  9894  qrevaddcl  9922  irradd  9924  irrmul  9925  ltsubrp  9969  ltaddrp  9970  xnn0xadd0  10146  icoshft  10269  fzen  10323  elfzm11  10371  uzsplit  10372  fzoval  10428  elfzom1elp1fzo  10493  exfzdc  10532  modaddmodup  10695  frec2uzrdg  10717  nninfinf  10751  seq3clss  10779  monoord  10793  seq3caopr3  10799  seqcaopr3g  10800  seq3f1olemp  10823  seqf1oglem2a  10826  seqf1og  10829  seq3id3  10832  seq3homo  10835  seq3z  10836  seqfeq4g  10839  ser3ge0  10844  expadd  10889  expmul  10892  leexp1a  10902  modqexp  10974  faccl  11043  facdiv  11046  faclbnd  11049  faclbnd6  11052  omgadd  11111  hashunsng  11117  seq3coll  11152  fundm2domnop0  11158  swrdswrdlem  11334  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccat3  11364  shftlem  11439  resqrexlemover  11633  resqrexlemdecn  11635  resqrexlemlo  11636  resqrexlemcalc3  11639  climub  11967  climserle  11968  fsumzcl2  12029  fsumsplitsnun  12043  fsum2d  12059  modfsummodlemstep  12081  fsumabs  12089  fsumiun  12101  bcxmas  12113  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  prodfap0  12169  prodfrecap  12170  ntrivcvgap  12172  prodmodc  12202  fprodssdc  12214  fprodabs  12240  fprod2d  12247  dvdsmod0  12417  dvds2ln  12448  dvdsabseq  12471  dvdsdivcl  12474  alzdvds  12478  oddnn02np1  12504  m1exp1  12525  nn0o1gt2  12529  nno  12530  ndvdsadd  12555  flodddiv4  12560  bitsinv1  12586  gcddiv  12653  gcdmultiple  12654  gcdmultiplez  12655  rplpwr  12661  dvdssq  12665  nninfct  12675  nn0seqcvgd  12676  alginv  12682  algcvga  12686  algfx  12687  isprm2  12752  isprm3  12753  prmdvdsexp  12783  eulerthlemrprm  12864  eulerthlema  12865  pcmpt  12979  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemhom  13099  omiunct  13128  nninfdclemlt  13135  setsn0fun  13182  mgmcl  13505  dfgrp3mlem  13744  mhmmulg  13813  resghm2b  13912  gsumfzconst  13991  srgpcomp  14067  lmodfopnelem1  14403  rmodislmodlem  14429  lss1d  14462  cnfldmulg  14655  cnfldexp  14656  gsumfzfsumlemm  14666  restopnb  14975  restdis  14978  tgcnp  15003  cnntr  15019  cnsscnp  15023  txcn  15069  txlm  15073  mettri  15167  blssexps  15223  blssex  15224  mopni3  15278  metss  15288  dvmptfsum  15519  plycolemc  15552  rpcxpmul2  15707  gausslemma2dlem6  15869  lgsquad2lem2  15884  2lgslem1c  15892  2lgslem3  15903  2lgs  15906  uhgredgrnv  16062  usgruspgrben  16110  usgredg2vlem2  16147  subupgr  16197  uspgr2wlkeq  16289  clwwlkccatlem  16324  umgrclwwlkge2  16326  clwwlkn1loopb  16344  clwwlknonex2lem2  16362  eupth2lem3lem4fi  16397  eupth2fi  16403  2spim  16467  exmidcon  16711