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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  mpan9  279  19.41h  1673  19.41  1674  equtr2  1699  mopick  2092  2euex  2101  gencl  2758  2gencl  2759  rspccva  2829  indifdir  3378  sseq0  3450  minel  3470  r19.2m  3495  r19.2mOLD  3496  elelpwi  3571  ssuni  3811  disjiun  3977  trintssm  4096  ssexg  4121  pofun  4290  sowlin  4298  2optocl  4681  3optocl  4682  elrnmpt1  4855  resieq  4894  fnun  5294  fss  5349  fun  5360  dmfex  5377  fvelimab  5542  mptfvex  5571  fmptco  5651  fnressn  5671  fressnfv  5672  fvtp2g  5694  fvtp3g  5695  fnex  5707  funfvima3  5718  isores3  5783  f1o2ndf1  6196  reldmtpos  6221  smores  6260  tfrlem7  6285  tfrlemi1  6300  tfrexlem  6302  tfrcl  6332  frecrdg  6376  nnacl  6448  nnmcl  6449  nnmsucr  6456  nntri3or  6461  nnaword  6479  nnaordex  6495  2ecoptocl  6589  ssct  6784  enm  6786  xpf1o  6810  ac6sfi  6864  f1dmvrnfibi  6909  f1vrnfibi  6910  updjud  7047  enumct  7080  nnnninfeq  7092  exmidontriimlem4  7180  exmidontriim  7181  elni2  7255  ax1rid  7818  negf1o  8280  mulgt1  8758  lbreu  8840  nnaddcl  8877  nnmulcl  8878  zaddcllempos  9228  zaddcllemneg  9230  nn0n0n1ge2b  9270  fzind  9306  fnn0ind  9307  uzaddcl  9524  elpq  9586  uzsubsubfz  9982  elfz1b  10025  elfz0ubfz0  10060  fz0fzdiffz0  10065  elfzmlbp  10067  fzofzim  10123  elfzom1elp1fzo  10137  elfzom1p1elfzo  10149  ssfzo12bi  10160  modfzo0difsn  10330  seq3val  10393  seqvalcd  10394  expcllem  10466  expap0  10485  apexp1  10631  faclbnd  10654  faclbnd6  10657  fihashf1rn  10702  omgadd  10715  hashfzp1  10737  seq3coll  10755  cjexp  10835  r19.29uz  10934  resqrexlemover  10952  resqrexlemlo  10955  resqrexlemcalc3  10958  absexp  11021  fimaxre2  11168  climshft  11245  climub  11285  climserle  11286  sumfct  11315  isumss2  11334  binom  11425  bcxmas  11430  clim2prod  11480  prodfap0  11486  prodfrecap  11487  prodfct  11528  demoivreALT  11714  dvdsdivcl  11788  dvdsfac  11798  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  m1exp1  11838  nn0o  11844  flodddiv4  11871  gcdneg  11915  bezoutlemmain  11931  dfgcd2  11947  gcdmultiple  11953  nnwosdc  11972  alginv  11979  cncongr1  12035  prmdvdsexp  12080  prmndvdsfaclt  12088  clsss  12758  xmettri2  13001  mettri  13013  metss  13134  zabsle1  13540  bdssexg  13786  bj-findis  13861  nninfalllem1  13888  nninfsellemdc  13890  redc0  13936