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  6077  supisoti  7011  caucvgsrlemoffres  7801  prodge0  8813  un0addcl  9211  un0mulcl  9212  peano2uz2  9362  elfz2nn0  10114  fzind2  10241  expaddzap  10566  expmulzap  10568  cau3lem  11125  climuni  11303  climrecvg1n  11358  fisumcom2  11448  fprodcom2fi  11636  dvdsval2  11799  algcvga  12053  lcmgcdlem  12079  divgcdcoprmex  12104  prmpwdvds  12355  isgrpinv  12931  dvdsrcl2  13273  islss4  13474  epttop  13629  cncnp  13769  cnconst  13773  bl2in  13942  metcnpi  14054  metcnpi2  14055  metcnpi3  14056