Theorem impr 379

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 115	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 257	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

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  ax-ia3 108

This theorem is referenced by:  reximddv2  2649  moi2  3001  preq12bg  3882  ordsuc  4690  f1ocnv2d  6267  f1o3d  6271  suppssrst  6474  suppssrgst  6475  supisoti  7314  caucvgsrlemoffres  8131  prodge0  9148  un0addcl  9549  un0mulcl  9550  peano2uz2  9706  elfz2nn0  10471  fzind2  10610  expaddzap  10972  expmulzap  10974  swrdswrd  11425  cau3lem  11827  climuni  12006  climrecvg1n  12061  fisumcom2  12152  fprodcom2fi  12340  dvdsval2  12504  algcvga  12776  lcmgcdlem  12802  divgcdcoprmex  12827  prmpwdvds  13081  isgrpinv  13812  gfsumval  14105  dvdsrcl2  14347  islss4  14659  lspsnel6  14685  epttop  15084  cncnp  15224  cnconst  15228  bl2in  15397  metcnpi  15509  metcnpi2  15510  metcnpi3  15511  perfect  15998  lgsquad2  16085  egrsubgr  16387  clwwlkccat  16525