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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  mpan9  281  19.41h  1737  19.41  1738  equtr2  1763  mopick  2165  2euex  2174  gencl  2854  2gencl  2855  vtocl4g  2894  vtocl4ga  2895  rspccva  2928  indifdir  3487  minel  3586  r19.2m  3614  r19.2mOLD  3615  elelpwi  3701  ssuni  3957  disjiun  4125  trintssm  4245  ssexg  4272  pofun  4457  sowlin  4465  2optocl  4852  3optocl  4853  ssrelrn  4972  elrnmpt1  5033  resieq  5073  fnun  5489  fss  5546  fun  5561  dmfex  5582  fvelimab  5759  mptfvex  5791  fmptco  5874  fnressn  5901  fressnfv  5902  fvtp2g  5924  fvtp3g  5925  fnex  5937  funfvima3  5952  isores3  6021  f1o2ndf1  6464  funsssuppss  6498  reldmtpos  6524  smores  6563  tfrlem7  6588  tfrlemi1  6603  tfrexlem  6605  tfrcl  6635  frecrdg  6679  nnacl  6753  nnmcl  6754  nnmsucr  6761  nntri3or  6766  nnaword  6784  nnaordex  6801  2ecoptocl  6897  ssct  7114  enm  7118  xpf1o  7144  ac6sfi  7202  f1dmvrnfibi  7258  f1vrnfibi  7259  suppeqfsuppbi  7295  updjud  7422  enumct  7455  nnnninfeq  7468  exmidontriimlem4  7580  exmidontriim  7581  elni2  7681  ax1rid  8244  negf1o  8709  mulgt1  9193  lbreu  9275  nnaddcl  9324  nnmulcl  9325  zaddcllempos  9681  zaddcllemneg  9683  nn0n0n1ge2b  9725  fzind  9761  fnn0ind  9762  uzaddcl  9986  elpq  10049  uzsubsubfz  10452  elfz1b  10497  elfz0ubfz0  10532  fz0fzdiffz0  10537  elfzmlbp  10539  fzofzim  10600  elfzom1elp1fzo  10620  elfzom1p1elfzo  10632  ssfzo12bi  10643  modfzo0difsn  10832  seq3val  10897  seqvalcd  10898  expcllem  10987  expap0  11006  apexp1  11156  faclbnd  11179  faclbnd6  11182  fihashf1rn  11227  omgadd  11242  hashfzp1  11265  hashmap  11268  seq3coll  11294  fundm2domnop0  11300  lswlgt0cl  11357  ccatsymb  11370  swrdnd  11431  swrd0g  11432  swrdspsleq  11439  pfxsuff1eqwrdeq  11471  swrdswrdlem  11476  swrdswrd  11477  wrd2ind  11495  pfxccatin12lem2a  11499  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  pfxccat3a  11510  swrdccat3blem  11511  cjexp  11658  r19.29uz  11758  resqrexlemover  11776  resqrexlemlo  11779  resqrexlemcalc3  11782  absexp  11845  fimaxre2  11993  climshft  12070  climub  12110  climserle  12111  sumfct  12140  isumss2  12160  binom  12251  bcxmas  12256  clim2prod  12306  prodfap0  12312  prodfrecap  12313  prodfct  12354  demoivreALT  12541  dvdsdivcl  12617  dvdsfac  12627  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  m1exp1  12668  nn0o  12674  flodddiv4  12703  gcdneg  12759  bezoutlemmain  12775  dfgcd2  12791  gcdmultiple  12797  nnwosdc  12816  alginv  12825  cncongr1  12881  prmdvdsexp  12926  prmndvdsfaclt  12934  dfgrp2  13832  srgmulgass  14293  lmodvsmmulgdi  14660  lmodfopnelem1  14661  rmodislmodlem  14687  cnfldmulg  14913  cnfldexp  14914  assamulgscm  15043  clsss  15219  xmettri2  15462  mettri  15474  metss  15595  plycolemc  15859  zabsle1  16118  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  2lgslem1a1  16205  incistruhgr  16331  umgrislfupgrenlem  16371  uhgr2edg  16447  usgredg2vlem2  16464  subgrfun  16508  wlkl1loop  16599  wlkres  16620  clwwlkccatlem  16641  isclwwlknx  16657  clwwlkext2edg  16663  clwwlknonel  16673  clwwlknonex2lem2  16679  clwwlknun  16682  depindlem2  16748  depindlem3  16749  bdssexg  16930  bj-findis  17005  nninfalllem1  17051  nninfsellemdc  17053  redc0  17107