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  1635  cbval2  1933  cbvex2  1934  nelelne  2456  r19.21be  2585  r19.35-1  2644  mosubt  2938  sbcrext  3064  uneqdifeqim  3533  ssuni  3858  uniss2  3867  elpwuni  4003  elssabg  4178  elpw2g  4186  epelg  4322  elomssom  4638  relop  4813  riinint  4924  cnviinm  5208  funopg  5289  fun  5427  tz6.12c  5585  fvelrnb  5605  fmptco  5725  fnressn  5745  fressnfv  5746  fvtp2g  5768  fvtp3g  5769  fconst2g  5774  isores3  5859  isoselem  5864  eloprabga  6006  fo1stresm  6216  poxp  6287  brtpos2  6306  smores  6347  tfrlem1  6363  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  frecrdg  6463  oawordriexmid  6525  nnacl  6535  nnmcl  6536  nnacom  6539  nnaass  6540  nnmsucr  6543  nndifsnid  6562  nnmordi  6571  iinerm  6663  th3qlem2  6694  elpmg  6720  pmss12g  6731  mapsn  6746  brdomg  6804  f1domg  6814  ssdomg  6834  nndomo  6922  elfi2  7033  nnnninfeq2  7190  carden2bex  7251  cc3  7330  addclpi  7389  addnidpig  7398  genpassl  7586  genpassu  7587  nqprloc  7607  ltaprlem  7680  recexprlemopl  7687  recexprlemopu  7689  recexprlemupu  7690  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemupu  7711  caucvgprlemupu  7734  caucvgprprlemupu  7762  archsr  7844  peano2nnnn  7915  receuap  8690  peano2nn  8996  nnaddcl  9004  zrevaddcl  9370  nzadd  9372  zdiv  9408  nneo  9423  zeo2  9426  peano5uzti  9428  fzind  9435  fnn0ind  9436  lbzbi  9684  qrevaddcl  9712  irradd  9714  irrmul  9715  ltsubrp  9759  ltaddrp  9760  xnn0xadd0  9936  icoshft  10059  fzen  10112  elfzm11  10160  uzsplit  10161  fzoval  10217  elfzom1elp1fzo  10272  exfzdc  10310  modaddmodup  10461  frec2uzrdg  10483  nninfinf  10517  seq3clss  10545  monoord  10559  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemp  10589  seqf1oglem2a  10592  seqf1og  10595  seq3id3  10598  seq3homo  10601  seq3z  10602  seqfeq4g  10605  ser3ge0  10610  expadd  10655  expmul  10658  leexp1a  10668  modqexp  10740  faccl  10809  facdiv  10812  faclbnd  10815  faclbnd6  10818  omgadd  10876  hashunsng  10881  seq3coll  10916  shftlem  10963  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc3  11163  climub  11490  climserle  11491  fsumzcl2  11551  fsumsplitsnun  11565  fsum2d  11581  modfsummodlemstep  11603  fsumabs  11611  fsumiun  11623  bcxmas  11635  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  prodfap0  11691  prodfrecap  11692  ntrivcvgap  11694  prodmodc  11724  fprodssdc  11736  fprodabs  11762  fprod2d  11769  dvdsmod0  11939  dvds2ln  11970  dvdsabseq  11992  dvdsdivcl  11995  alzdvds  11999  oddnn02np1  12024  m1exp1  12045  nn0o1gt2  12049  nno  12050  ndvdsadd  12075  flodddiv4  12078  gcddiv  12159  gcdmultiple  12160  gcdmultiplez  12161  rplpwr  12167  dvdssq  12171  nninfct  12181  nn0seqcvgd  12182  alginv  12188  algcvga  12192  algfx  12193  isprm2  12258  isprm3  12259  prmdvdsexp  12289  eulerthlemrprm  12370  eulerthlema  12371  pcmpt  12484  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemhom  12575  omiunct  12604  nninfdclemlt  12611  setsn0fun  12658  mgmcl  12945  dfgrp3mlem  13173  mhmmulg  13236  resghm2b  13335  gsumfzconst  13414  srgpcomp  13489  lmodfopnelem1  13823  rmodislmodlem  13849  lss1d  13882  cnfldmulg  14075  cnfldexp  14076  gsumfzfsumlemm  14086  restopnb  14360  restdis  14363  tgcnp  14388  cnntr  14404  cnsscnp  14408  txcn  14454  txlm  14458  mettri  14552  blssexps  14608  blssex  14609  mopni3  14663  metss  14673  dvmptfsum  14904  plycolemc  14936  gausslemma2dlem6  15224  lgsquad2lem2  15239  2lgslem1c  15247  2lgslem3  15258  2lgs  15261  2spim  15328