Theorem impr 649

Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
impr.1	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Assertion

Ref	Expression
impr	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Proof of Theorem impr

Step	Hyp	Ref	Expression
1		impr.1	. . 3 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 449	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  reximddv2  3020  moi2  3387  preq12bg  4386  prel12g  4387  disjxiun  4649  disjxiunOLD  4650  disjxun  4651  wereu2  5111  f1ocnv2d  6886  extmptsuppeq  7319  suppssr  7326  omeulem1  7662  oelim2  7675  oeoa  7677  boxriin  7950  frfi  8205  fipreima  8272  marypha1lem  8339  supiso  8381  ordtypelem10  8432  r1ordg  8641  infxpenc2lem1  8842  acndom  8874  acndom2  8877  cofsmo  9091  cfcoflem  9094  fin23lem28  9162  fin23lem36  9170  isf32lem1  9175  isf32lem2  9176  isf32lem5  9179  isf34lem4  9199  fin1a2lem6  9227  fin1a2s  9236  ttukeylem2  9332  ttukeylem6  9336  fpwwe2lem8  9459  fpwwe2lem12  9463  inar1  9597  grudomon  9639  axpre-sup  9990  prodge0  10870  un0addcl  11326  un0mulcl  11327  peano2uz2  11465  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  xlemul1a  12118  fzadd2  12376  elfz2nn0  12431  fzind2  12586  expaddz  12904  expmulz  12906  swrdswrd  13460  swrdccatin12lem2c  13488  swrdccatin12  13491  cau3lem  14094  lo1bdd2  14255  climuni  14283  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  dvdsval2  14986  algcvga  15292  lcmgcdlem  15319  coprmproddvdslem  15376  divgcdcoprmex  15380  iserodd  15540  prmpwdvds  15608  ram0  15726  catpropd  16369  mrcmndind  17366  isgrpinv  17472  gicsubgen  17721  sylow2alem2  18033  sylow2a  18034  frgpuptinv  18184  ablfac1eu  18472  dvdsrcl2  18650  islss4  18962  lspsnel6  18994  lmhmima  19047  lsmcl  19083  gsumbagdiag  19376  psrass1lem  19377  coe1tmmul2  19646  psgnodpm  19934  dsmmlss  20088  islindf4  20177  gsumcom3fi  20206  dmatscmcl  20309  mdetdiaglem  20404  mdetunilem9  20426  pm2mp  20630  epttop  20813  neindisj  20921  neitr  20984  restcls  20985  restntr  20986  ordtrest2lem  21007  cncnp  21084  cnconst  21088  1stcrest  21256  2ndcdisj  21259  2ndcsep  21262  1stccnp  21265  islly2  21287  1stckgenlem  21356  ptbasin  21380  ptbasfi  21384  ptcnplem  21424  ptcnp  21425  tx1stc  21453  qtophmeo  21620  filconn  21687  filuni  21689  ufileu  21723  elfm3  21754  rnelfmlem  21756  fmfnfmlem4  21761  cnpflf2  21804  alexsubALTlem4  21854  ptcmplem3  21858  ptcmplem4  21859  ptcmplem5  21860  tsmsxplem1  21956  bl2in  22205  metcnpi  22349  metcnpi2  22350  metcnpi3  22351  recld2  22617  icoopnst  22738  iocopnst  22739  ncvs1  22957  iscfil3  23071  iscmet3lem2  23090  ovoliunlem1  23270  ovolicc2lem2  23286  ovolicc2lem4  23288  voliun  23322  volsuplem  23323  dyadmbllem  23367  mbfinf  23432  mbflimsup  23433  itg2seq  23509  itg2splitlem  23515  itg2cnlem1  23528  ellimc3  23643  dvnadd  23692  dvcnvlem  23739  c1liplem1  23759  lhop2  23778  coe1mul3  23859  ply1divex  23896  dvdsq1p  23920  aannenlem1  24083  aalioulem2  24088  dvtaylp  24124  ulmdvlem3  24156  iblulm  24161  cxpmul2z  24437  leibpilem1  24667  xrlimcnp  24695  lgambdd  24763  wilthlem2  24795  basellem3  24809  dvdsflsumcom  24914  perfect  24956  dchreq  24983  dchrsum  24994  bposlem1  25009  lgsquad2  25111  dchrisum0fno1  25200  pntibnd  25282  lmieu  25676  ax5seglem5  25813  axeuclid  25843  egrsubgr  26169  nbumgrvtx  26242  wwlksnextsur  26795  wwlksext2clwwlk  26924  nmcvcn  27550  ubthlem1  27726  leopmul2i  28994  hstel2  29078  atom1d  29212  cdj1i  29292  f1o3d  29431  xrge0addge  29522  reff  29906  ordtrest2NEWlem  29968  esumcst  30125  eulerpartlemgh  30440  cvmscld  31255  cgrxfr  32162  finminlem  32312  nn0prpwlem  32317  neibastop1  32354  neibastop2lem  32355  tailfb  32372  finixpnum  33394  lindsenlbs  33404  matunitlindflem2  33406  poimirlem4  33413  poimirlem25  33434  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  heicant  33444  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnclem3  33463  ftc1anc  33493  subspopn  33548  prdsbnd  33592  heibor1lem  33608  heiborlem1  33610  heibor  33620  isdrngo2  33757  rngoisocnv  33780  maxidlmax  33842  riotasv3d  34246  lkrpssN  34450  intnatN  34693  elpaddatiN  35091  pexmidlem5N  35260  lhpj1  35308  ltrnu  35407  cdlemn11pre  36499  dihord2pre  36514  dih1dimatlem0  36617  lcfrlem9  36839  rexrabdioph  37358  ctbnfien  37382  irrapxlem3  37388  elpell14qr2  37426  elpell1qr2  37436  kelac1  37633  iunrelexpuztr  38011  rfovcnvfvd  38301  radcnvrat  38513  nznngen  38515  tz6.12-afv  41253  iccelpart  41369  pfxccatin12  41425  lighneallem4  41527  perfectALTV  41632  bgoldbtbndlem3  41695  tgoldbach  41705  tgoldbachOLD  41712  isassintop  41846  ellcoellss  42224  lindslinindsimp2  42252  aacllem  42547