Theorem impcom 124

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 123	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  mpan9  276  19.41h  1627  19.41  1628  equtr2  1651  mopick  2033  2euex  2042  gencl  2665  2gencl  2666  rspccva  2735  indifdir  3271  sseq0  3343  minel  3363  r19.2m  3388  r19.2mOLD  3389  elelpwi  3461  ssuni  3697  disjiun  3862  trintssm  3974  ssexg  3999  pofun  4163  sowlin  4171  2optocl  4544  3optocl  4545  elrnmpt1  4718  resieq  4755  fnun  5154  fss  5207  fun  5218  dmfex  5235  fvelimab  5395  mptfvex  5424  fmptco  5503  fnressn  5522  fressnfv  5523  fvtp2g  5545  fvtp3g  5546  fnex  5558  funfvima3  5567  isores3  5632  f1o2ndf1  6031  reldmtpos  6056  smores  6095  tfrlem7  6120  tfrlemi1  6135  tfrexlem  6137  tfrcl  6167  frecrdg  6211  nnacl  6281  nnmcl  6282  nnmsucr  6289  nntri3or  6294  nnaword  6310  nnaordex  6326  2ecoptocl  6420  ssct  6614  enm  6616  xpf1o  6640  ac6sfi  6694  f1dmvrnfibi  6733  f1vrnfibi  6734  updjud  6853  enumct  6873  elni2  6970  ax1rid  7509  negf1o  7957  mulgt1  8421  lbreu  8503  nnaddcl  8540  nnmulcl  8541  zaddcllempos  8885  zaddcllemneg  8887  nn0n0n1ge2b  8924  fzind  8960  fnn0ind  8961  uzaddcl  9173  uzsubsubfz  9610  elfz1b  9653  elfz0ubfz0  9685  fz0fzdiffz0  9690  elfzmlbp  9692  fzofzim  9748  elfzom1elp1fzo  9762  elfzom1p1elfzo  9774  ssfzo12bi  9785  modfzo0difsn  9951  seq3val  10013  expcllem  10081  expap0  10100  faclbnd  10264  faclbnd6  10267  fihashf1rn  10312  omgadd  10325  hashfzp1  10347  seq3coll  10362  cjexp  10442  r19.29uz  10540  resqrexlemover  10558  resqrexlemlo  10561  resqrexlemcalc3  10564  absexp  10627  fimaxre2  10773  climshft  10847  climub  10887  climserle  10888  sumfct  10917  isumss2  10936  binom  11027  bcxmas  11032  demoivreALT  11212  dvdsdivcl  11278  dvdsfac  11288  oddnn02np1  11307  oddge22np1  11308  evennn02n  11309  evennn2n  11310  m1exp1  11328  nn0o  11334  flodddiv4  11361  gcdneg  11400  bezoutlemmain  11414  dfgcd2  11430  gcdmultiple  11436  alginv  11456  cncongr1  11512  prmdvdsexp  11554  prmndvdsfaclt  11562  clsss  11970  xmettri2  12147  mettri  12159  metss  12280  bdssexg  12503  bj-findis  12582  nninfalllemn  12603  nninfalllem1  12604  nninfsellemdc  12607