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  1575  19.41  1576  equtr2  1597  mopick  1978  2euex  1987  gencl  2586  2gencl  2587  rspccva  2655  sbcimdv  2823  indifdir  3193  sseq0  3258  minel  3283  r19.2m  3309  elelpwi  3370  ssuni  3602  trint0m  3871  ssexg  3896  pofun  4049  sowlin  4057  2optocl  4417  3optocl  4418  elrnmpt1  4585  resieq  4622  fnun  5005  fss  5054  fun  5063  dmfex  5079  fvelimab  5229  mptfvex  5256  fmptco  5330  fnressn  5349  fressnfv  5350  fvtp2g  5370  fvtp3g  5371  fnex  5383  funfvima3  5392  isores3  5455  f1o2ndf1  5849  reldmtpos  5868  smores  5907  tfrlem7  5933  tfrlemi1  5946  tfrexlem  5948  rdgon  5973  frecrdg  5992  nnacl  6059  nnmcl  6060  nnmsucr  6067  nntri3or  6072  nnaword  6084  nnaordex  6100  2ecoptocl  6194  enm  6294  ac6sfi  6352  elni2  6412  ax1rid  6951  mulgt1  7829  nnaddcl  7934  nnmulcl  7935  zaddcllempos  8282  zaddcllemneg  8284  nn0n0n1ge2b  8320  fzind  8353  fnn0ind  8354  uzaddcl  8529  uzsubsubfz  8911  elfz1b  8952  elfz0ubfz0  8982  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  fzofzim  9044  elfzom1elp1fzo  9058  elfzom1p1elfzo  9070  ssfzo12bi  9081  iseqss  9226  expivallem  9256  expcllem  9266  expap0  9285  cjexp  9493  r19.29uz  9590  resqrexlemover  9608  resqrexlemlo  9611  resqrexlemcalc3  9614  absexp  9675  climshft  9825  climub  9864  climserile  9865  ialginv  9886  bdssexg  10024  bj-findis  10104