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  2635  moi2  2984  preq12bg  3851  ordsuc  4656  f1ocnv2d  6219  supisoti  7193  caucvgsrlemoffres  8003  prodge0  9017  un0addcl  9418  un0mulcl  9419  peano2uz2  9570  elfz2nn0  10325  fzind2  10462  expaddzap  10822  expmulzap  10824  swrdswrd  11258  cau3lem  11646  climuni  11825  climrecvg1n  11880  fisumcom2  11970  fprodcom2fi  12158  dvdsval2  12322  algcvga  12594  lcmgcdlem  12620  divgcdcoprmex  12645  prmpwdvds  12899  isgrpinv  13608  dvdsrcl2  14084  islss4  14367  lspsnel6  14393  epttop  14785  cncnp  14925  cnconst  14929  bl2in  15098  metcnpi  15210  metcnpi2  15211  metcnpi3  15212  perfect  15696  lgsquad2  15783  clwwlkccat  16170