Theorem impr 377

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 114	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 255	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  reximddv2  2575  moi2  2911  preq12bg  3758  ordsuc  4545  f1ocnv2d  6050  supisoti  6983  caucvgsrlemoffres  7749  prodge0  8757  un0addcl  9155  un0mulcl  9156  peano2uz2  9306  elfz2nn0  10055  fzind2  10182  expaddzap  10507  expmulzap  10509  cau3lem  11065  climuni  11243  climrecvg1n  11298  fisumcom2  11388  fprodcom2fi  11576  dvdsval2  11739  algcvga  11992  lcmgcdlem  12018  divgcdcoprmex  12043  prmpwdvds  12294  epttop  12805  cncnp  12945  cnconst  12949  bl2in  13118  metcnpi  13230  metcnpi2  13231  metcnpi3  13232