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  2611  moi2  2954  preq12bg  3814  ordsuc  4612  f1ocnv2d  6152  supisoti  7114  caucvgsrlemoffres  7915  prodge0  8929  un0addcl  9330  un0mulcl  9331  peano2uz2  9482  elfz2nn0  10236  fzind2  10370  expaddzap  10730  expmulzap  10732  cau3lem  11458  climuni  11637  climrecvg1n  11692  fisumcom2  11782  fprodcom2fi  11970  dvdsval2  12134  algcvga  12406  lcmgcdlem  12432  divgcdcoprmex  12457  prmpwdvds  12711  isgrpinv  13419  dvdsrcl2  13894  islss4  14177  lspsnel6  14203  epttop  14595  cncnp  14735  cnconst  14739  bl2in  14908  metcnpi  15020  metcnpi2  15021  metcnpi3  15022  perfect  15506  lgsquad2  15593