Theorem impcom 125

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
impcom	|- ( ( ps /\ ph ) -> ch )

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	com12 30	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 124	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-ia1 106  ax-ia2 107

This theorem is referenced by:  mpan9  281  19.41h  1709  19.41  1710  equtr2  1735  mopick  2134  2euex  2143  gencl  2809  2gencl  2810  vtocl4g  2849  vtocl4ga  2850  rspccva  2883  indifdir  3437  sseq0  3510  minel  3530  r19.2m  3555  r19.2mOLD  3556  elelpwi  3638  ssuni  3886  disjiun  4054  trintssm  4174  ssexg  4199  pofun  4377  sowlin  4385  2optocl  4770  3optocl  4771  ssrelrn  4888  elrnmpt1  4948  resieq  4988  fnun  5401  fss  5457  fun  5469  dmfex  5487  fvelimab  5658  mptfvex  5688  fmptco  5769  fnressn  5793  fressnfv  5794  fvtp2g  5816  fvtp3g  5817  fnex  5829  funfvima3  5841  isores3  5907  f1o2ndf1  6337  reldmtpos  6362  smores  6401  tfrlem7  6426  tfrlemi1  6441  tfrexlem  6443  tfrcl  6473  frecrdg  6517  nnacl  6589  nnmcl  6590  nnmsucr  6597  nntri3or  6602  nnaword  6620  nnaordex  6637  2ecoptocl  6733  ssct  6938  enm  6940  xpf1o  6966  ac6sfi  7021  f1dmvrnfibi  7072  f1vrnfibi  7073  updjud  7210  enumct  7243  nnnninfeq  7256  exmidontriimlem4  7367  exmidontriim  7368  elni2  7462  ax1rid  8025  negf1o  8489  mulgt1  8971  lbreu  9053  nnaddcl  9091  nnmulcl  9092  zaddcllempos  9444  zaddcllemneg  9446  nn0n0n1ge2b  9487  fzind  9523  fnn0ind  9524  uzaddcl  9742  elpq  9805  uzsubsubfz  10204  elfz1b  10247  elfz0ubfz0  10282  fz0fzdiffz0  10287  elfzmlbp  10289  fzofzim  10349  elfzom1elp1fzo  10368  elfzom1p1elfzo  10380  ssfzo12bi  10391  modfzo0difsn  10577  seq3val  10642  seqvalcd  10643  expcllem  10732  expap0  10751  apexp1  10900  faclbnd  10923  faclbnd6  10926  fihashf1rn  10970  omgadd  10984  hashfzp1  11006  seq3coll  11024  fundm2domnop0  11027  lswlgt0cl  11083  ccatsymb  11096  swrdnd  11150  swrd0g  11151  swrdspsleq  11158  pfxsuff1eqwrdeq  11190  swrdswrdlem  11195  swrdswrd  11196  wrd2ind  11214  pfxccatin12lem2a  11218  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  pfxccat3a  11229  swrdccat3blem  11230  cjexp  11319  r19.29uz  11418  resqrexlemover  11436  resqrexlemlo  11439  resqrexlemcalc3  11442  absexp  11505  fimaxre2  11653  climshft  11730  climub  11770  climserle  11771  sumfct  11800  isumss2  11819  binom  11910  bcxmas  11915  clim2prod  11965  prodfap0  11971  prodfrecap  11972  prodfct  12013  demoivreALT  12200  dvdsdivcl  12276  dvdsfac  12286  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  m1exp1  12327  nn0o  12333  flodddiv4  12362  gcdneg  12418  bezoutlemmain  12434  dfgcd2  12450  gcdmultiple  12456  nnwosdc  12475  alginv  12484  cncongr1  12540  prmdvdsexp  12585  prmndvdsfaclt  12593  dfgrp2  13474  srgmulgass  13866  lmodvsmmulgdi  14200  lmodfopnelem1  14201  rmodislmodlem  14227  cnfldmulg  14453  cnfldexp  14454  clsss  14705  xmettri2  14948  mettri  14960  metss  15081  plycolemc  15345  zabsle1  15591  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem3  15655  gausslemma2dlem4  15656  2lgslem1a1  15678  incistruhgr  15801  umgrislfupgrenlem  15836  bdssexg  16039  bj-findis  16114  nninfalllem1  16147  nninfsellemdc  16149  redc0  16198