Theorem expcom 114

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 113	. 2 |- ( ph -> ( ps -> ch ) )
3	2	com12 30	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  ancoms  264  syldan  276  sylan  277  pm4.79dc  842  dedlema  910  dedlemb  911  19.35-1  1555  cbval2  1837  cbvex2  1838  r19.21be  2452  r19.35-1  2504  mosubt  2769  sbcrext  2891  uneqdifeqim  3328  ssuni  3623  uniss2  3632  elpwuni  3762  elssabg  3923  elpw2g  3931  epelg  4045  elnn  4346  relop  4504  riinint  4611  cnviinm  4879  funopg  4954  fun  5083  tz6.12c  5224  fvelrnb  5242  fmptco  5351  fnressn  5370  fressnfv  5371  fvtp2g  5391  fvtp3g  5392  fconst2g  5397  isores3  5475  isoselem  5479  eloprabga  5611  fo1stresm  5808  poxp  5873  brtpos2  5889  smores  5930  tfrlem1  5946  tfrlemi1  5969  rdgon  5996  frecrdg  6015  freccl  6016  nnacl  6082  nnmcl  6083  nnacom  6086  nnaass  6087  nnmsucr  6090  nnmordi  6112  iinerm  6201  th3qlem2  6232  brdomg  6252  f1domg  6261  ssdomg  6281  nndomo  6350  carden2bex  6458  addclpi  6517  addnidpig  6526  genpassl  6714  genpassu  6715  nqprloc  6735  ltaprlem  6808  recexprlemopl  6815  recexprlemopu  6817  recexprlemupu  6818  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemupu  6839  caucvgprlemupu  6862  caucvgprprlemupu  6890  archsr  6958  peano2nnnn  7021  receuap  7759  peano2nn  8051  nnaddcl  8059  zrevaddcl  8401  nzadd  8403  zdiv  8435  nneo  8450  zeo2  8453  peano5uzti  8455  fzind  8462  fnn0ind  8463  lbzbi  8701  qrevaddcl  8729  irradd  8731  irrmul  8732  ltsubrp  8768  ltaddrp  8769  icoshft  9012  fzen  9062  elfzm11  9108  uzsplit  9109  fzoval  9158  elfzom1elp1fzo  9211  exfzdc  9249  modaddmodup  9389  frec2uzzd  9402  frec2uzrdg  9411  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqhomo  9468  iseqz  9469  expadd  9518  expmul  9521  leexp1a  9531  faccl  9662  facdiv  9665  faclbnd  9668  faclbnd6  9671  shftlem  9704  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  climub  10182  climserile  10183  dvds2ln  10228  dvdsabseq  10247  dvdsdivcl  10250  alzdvds  10254  oddnn02np1  10280  m1exp1  10301  nn0o1gt2  10305  nno  10306  ndvdsadd  10331  flodddiv4  10334  gcddiv  10408  gcdmultiple  10409  gcdmultiplez  10410  rplpwr  10416  dvdssq  10420  nn0seqcvgd  10423  ialginv  10429  ialgcvga  10433  ialgfx  10434  isprm2  10499  isprm3  10500  prmdvdsexp  10527  2spim  10577