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  2985  preq12bg  3854  ordsuc  4659  f1ocnv2d  6222  supisoti  7203  caucvgsrlemoffres  8013  prodge0  9027  un0addcl  9428  un0mulcl  9429  peano2uz2  9580  elfz2nn0  10340  fzind2  10478  expaddzap  10838  expmulzap  10840  swrdswrd  11279  cau3lem  11668  climuni  11847  climrecvg1n  11902  fisumcom2  11992  fprodcom2fi  12180  dvdsval2  12344  algcvga  12616  lcmgcdlem  12642  divgcdcoprmex  12667  prmpwdvds  12921  isgrpinv  13630  dvdsrcl2  14106  islss4  14389  lspsnel6  14415  epttop  14807  cncnp  14947  cnconst  14951  bl2in  15120  metcnpi  15232  metcnpi2  15233  metcnpi3  15234  perfect  15718  lgsquad2  15805  clwwlkccat  16210  gfsumval  16630