Theorem impcom 116

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 27	. 2 |- (ps -> (ph -> ch))
3	2	imp 115	1 |- ((ps /\ ph) -> ch)

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  mpan9  265  19.41h  1572  19.41  1573  equtr2  1594  mopick  1975  2euex  1984  gencl  2580  2gencl  2581  rspccva  2649  sbcimdv  2817  indifdir  3187  sseq0  3252  minel  3277  r19.2m  3303  elelpwi  3362  ssuni  3593  trint0m  3862  ssexg  3887  pofun  4040  sowlin  4048  2optocl  4360  3optocl  4361  elrnmpt1  4528  resieq  4565  fnun  4948  fss  4997  fun  5006  dmfex  5022  fvelimab  5172  mptfvex  5199  fmptco  5273  fnressn  5292  fressnfv  5293  fvtp2g  5313  fvtp3g  5314  fnex  5326  funfvima3  5335  isores3  5398  f1o2ndf1  5791  reldmtpos  5809  smores  5848  tfrlem7  5874  tfrlemi1  5887  tfrexlem  5889  rdgon  5913  frecrdg  5931  nnacl  5998  nnmcl  5999  nnmsucr  6006  nntri3or  6011  nnaword  6020  nnaordex  6036  2ecoptocl  6130  enm  6230  elni2  6298  ax1rid  6761  mulgt1  7610  nnaddcl  7715  nnmulcl  7716  zaddcllempos  8058  zaddcllemneg  8060  nn0n0n1ge2b  8096  fzind  8129  fnn0ind  8130  uzaddcl  8305  uzsubsubfz  8681  elfz1b  8722  elfz0ubfz0  8752  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  fzofzim  8814  elfzom1elp1fzo  8828  elfzom1p1elfzo  8840  ssfzo12bi  8851  expivallem  8910  expcllem  8920  expap0  8939  cjexp  9121  bdssexg  9359  bj-findis  9439