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  2582  moi2  2920  preq12bg  3775  ordsuc  4564  f1ocnv2d  6078  supisoti  7012  caucvgsrlemoffres  7802  prodge0  8814  un0addcl  9212  un0mulcl  9213  peano2uz2  9363  elfz2nn0  10115  fzind2  10242  expaddzap  10567  expmulzap  10569  cau3lem  11126  climuni  11304  climrecvg1n  11359  fisumcom2  11449  fprodcom2fi  11637  dvdsval2  11800  algcvga  12054  lcmgcdlem  12080  divgcdcoprmex  12105  prmpwdvds  12356  isgrpinv  12935  dvdsrcl2  13306  islss4  13507  lspsnel6  13533  epttop  13778  cncnp  13918  cnconst  13922  bl2in  14091  metcnpi  14203  metcnpi2  14204  metcnpi3  14205