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 )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  mpan9  281  19.41h  1731  19.41  1732  equtr2  1757  mopick  2156  2euex  2165  gencl  2832  2gencl  2833  vtocl4g  2872  vtocl4ga  2873  rspccva  2906  indifdir  3460  sseq0  3533  minel  3553  r19.2m  3578  r19.2mOLD  3579  elelpwi  3661  ssuni  3910  disjiun  4078  trintssm  4198  ssexg  4223  pofun  4403  sowlin  4411  2optocl  4796  3optocl  4797  ssrelrn  4914  elrnmpt1  4975  resieq  5015  fnun  5429  fss  5485  fun  5497  dmfex  5515  fvelimab  5690  mptfvex  5720  fmptco  5801  fnressn  5825  fressnfv  5826  fvtp2g  5848  fvtp3g  5849  fnex  5861  funfvima3  5873  isores3  5939  f1o2ndf1  6374  reldmtpos  6399  smores  6438  tfrlem7  6463  tfrlemi1  6478  tfrexlem  6480  tfrcl  6510  frecrdg  6554  nnacl  6626  nnmcl  6627  nnmsucr  6634  nntri3or  6639  nnaword  6657  nnaordex  6674  2ecoptocl  6770  ssct  6975  enm  6979  xpf1o  7005  ac6sfi  7060  f1dmvrnfibi  7111  f1vrnfibi  7112  updjud  7249  enumct  7282  nnnninfeq  7295  exmidontriimlem4  7406  exmidontriim  7407  elni2  7501  ax1rid  8064  negf1o  8528  mulgt1  9010  lbreu  9092  nnaddcl  9130  nnmulcl  9131  zaddcllempos  9483  zaddcllemneg  9485  nn0n0n1ge2b  9526  fzind  9562  fnn0ind  9563  uzaddcl  9781  elpq  9844  uzsubsubfz  10243  elfz1b  10286  elfz0ubfz0  10321  fz0fzdiffz0  10326  elfzmlbp  10328  fzofzim  10388  elfzom1elp1fzo  10408  elfzom1p1elfzo  10420  ssfzo12bi  10431  modfzo0difsn  10617  seq3val  10682  seqvalcd  10683  expcllem  10772  expap0  10791  apexp1  10940  faclbnd  10963  faclbnd6  10966  fihashf1rn  11010  omgadd  11024  hashfzp1  11046  seq3coll  11064  fundm2domnop0  11067  lswlgt0cl  11124  ccatsymb  11137  swrdnd  11191  swrd0g  11192  swrdspsleq  11199  pfxsuff1eqwrdeq  11231  swrdswrdlem  11236  swrdswrd  11237  wrd2ind  11255  pfxccatin12lem2a  11259  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  pfxccat3a  11270  swrdccat3blem  11271  cjexp  11404  r19.29uz  11503  resqrexlemover  11521  resqrexlemlo  11524  resqrexlemcalc3  11527  absexp  11590  fimaxre2  11738  climshft  11815  climub  11855  climserle  11856  sumfct  11885  isumss2  11904  binom  11995  bcxmas  12000  clim2prod  12050  prodfap0  12056  prodfrecap  12057  prodfct  12098  demoivreALT  12285  dvdsdivcl  12361  dvdsfac  12371  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  m1exp1  12412  nn0o  12418  flodddiv4  12447  gcdneg  12503  bezoutlemmain  12519  dfgcd2  12535  gcdmultiple  12541  nnwosdc  12560  alginv  12569  cncongr1  12625  prmdvdsexp  12670  prmndvdsfaclt  12678  dfgrp2  13560  srgmulgass  13952  lmodvsmmulgdi  14287  lmodfopnelem1  14288  rmodislmodlem  14314  cnfldmulg  14540  cnfldexp  14541  clsss  14792  xmettri2  15035  mettri  15047  metss  15168  plycolemc  15432  zabsle1  15678  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem3  15742  gausslemma2dlem4  15743  2lgslem1a1  15765  incistruhgr  15890  umgrislfupgrenlem  15928  uhgr2edg  16004  usgredg2vlem2  16021  wlkl1loop  16069  bdssexg  16267  bj-findis  16342  nninfalllem1  16374  nninfsellemdc  16376  redc0  16425