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  4655  f1ocnv2d  6216  supisoti  7185  caucvgsrlemoffres  7995  prodge0  9009  un0addcl  9410  un0mulcl  9411  peano2uz2  9562  elfz2nn0  10316  fzind2  10453  expaddzap  10813  expmulzap  10815  swrdswrd  11245  cau3lem  11633  climuni  11812  climrecvg1n  11867  fisumcom2  11957  fprodcom2fi  12145  dvdsval2  12309  algcvga  12581  lcmgcdlem  12607  divgcdcoprmex  12632  prmpwdvds  12886  isgrpinv  13595  dvdsrcl2  14071  islss4  14354  lspsnel6  14380  epttop  14772  cncnp  14912  cnconst  14916  bl2in  15085  metcnpi  15197  metcnpi2  15198  metcnpi3  15199  perfect  15683  lgsquad2  15770