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  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  3610  ssuni  3952  uniss2  3961  elpwuni  4097  elssabg  4279  elpw2g  4287  epelg  4430  elomssom  4747  relop  4925  riinint  5038  cnviinm  5324  funopg  5406  fun  5556  tz6.12c  5720  fvelrnb  5744  fmptco  5865  funopsn  5882  fnressn  5892  fressnfv  5893  fvtp2g  5915  fvtp3g  5916  fconst2g  5921  isores3  6011  isoselem  6016  eloprabga  6165  fo1stresm  6385  poxp  6458  fsuppeq  6477  suppssdc  6490  brtpos2  6512  smores  6553  tfrlem1  6569  tfrlemi1  6593  tfr1onlemaccex  6609  tfrcllemaccex  6622  frecrdg  6669  oawordriexmid  6733  nnacl  6743  nnmcl  6744  nnacom  6747  nnaass  6748  nnmsucr  6751  nndifsnid  6770  nnmordi  6779  iinerm  6871  th3qlem2  6902  elpmg  6928  pmss12g  6946  mapsn  6962  brdomg  7022  f1domg  7034  ssdomg  7055  nndomo  7155  ffsuppbi  7290  elfi2  7296  nnnninfeq2  7459  carden2bex  7525  cc3  7624  addclpi  7684  addnidpig  7693  genpassl  7881  genpassu  7882  nqprloc  7902  ltaprlem  7975  recexprlemopl  7982  recexprlemopu  7984  recexprlemupu  7985  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemupu  8006  caucvgprlemupu  8029  caucvgprprlemupu  8057  archsr  8139  peano2nnnn  8210  receuap  8989  peano2nn  9295  nnaddcl  9303  zrevaddcl  9674  nzadd  9676  zdiv  9713  nneo  9728  zeo2  9731  peano5uzti  9733  fzind  9740  fnn0ind  9741  lbzbi  9995  qrevaddcl  10023  irradd  10025  irrmul  10026  ltsubrp  10070  ltaddrp  10071  xnn0xadd0  10248  icoshft  10371  fzen  10426  elfzm11  10476  uzsplit  10477  fzoval  10533  elfzom1elp1fzo  10598  exfzdc  10637  modaddmodup  10802  frec2uzrdg  10824  nninfinf  10858  seq3clss  10886  monoord  10900  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemp  10930  seqf1oglem2a  10933  seqf1og  10936  seq3id3  10939  seq3homo  10942  seq3z  10943  seqfeq4g  10946  ser3ge0  10951  expadd  10996  expmul  10999  leexp1a  11009  modqexp  11082  faccl  11151  facdiv  11154  faclbnd  11157  faclbnd6  11160  omgadd  11220  hashunsng  11226  hashmap  11246  hashf1  11265  seq3coll  11272  fundm2domnop0  11278  swrdswrdlem  11454  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccat3  11484  shftlem  11559  resqrexlemover  11754  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc3  11760  climub  12088  climserle  12089  fsumzcl2  12150  fsumsplitsnun  12164  fsum2d  12180  modfsummodlemstep  12202  fsumabs  12210  fsumiun  12222  bcxmas  12234  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  prodfap0  12290  prodfrecap  12291  ntrivcvgap  12293  prodmodc  12323  fprodssdc  12335  fprodabs  12361  fprod2d  12368  dvdsmod0  12538  dvds2ln  12569  dvdsabseq  12592  dvdsdivcl  12595  alzdvds  12599  oddnn02np1  12625  m1exp1  12646  nn0o1gt2  12650  nno  12651  ndvdsadd  12676  flodddiv4  12681  bitsinv1  12707  gcddiv  12774  gcdmultiple  12775  gcdmultiplez  12776  rplpwr  12782  dvdssq  12786  nninfct  12796  nn0seqcvgd  12797  alginv  12803  algcvga  12807  algfx  12808  isprm2  12873  isprm3  12874  prmdvdsexp  12904  eulerthlemrprm  12985  eulerthlema  12986  pcmpt  13100  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemhom  13284  omiunct  13313  nninfdclemlt  13320  setsn0fun  13367  mgmcl  13656  dfgrp3mlem  13880  mhmmulg  13943  resghm2b  14042  gzsumconst  14120  srgpcomp  14268  lmodfopnelem1  14633  rmodislmodlem  14659  lss1d  14692  cnfldmulg  14885  cnfldexp  14886  restopnb  15205  restdis  15208  tgcnp  15233  cnntr  15249  cnsscnp  15253  txcn  15299  txlm  15303  mettri  15397  blssexps  15453  blssex  15454  mopni3  15508  metss  15518  dvmptfsum  15749  plycolemc  15782  rpcxpmul2  15938  gausslemma2dlem6  16100  lgsquad2lem2  16115  2lgslem1c  16123  2lgslem3  16134  2lgs  16137  uhgredgrnv  16293  usgruspgrben  16341  usgredg2vlem2  16378  subupgr  16428  uspgr2wlkeq  16520  clwwlkccatlem  16555  umgrclwwlkge2  16557  clwwlkn1loopb  16575  clwwlknonex2lem2  16593  eupth2lem3lem4fi  16628  eupth2fi  16634  2spim  16708  exmidcon  16950