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  3760  ordsuc  4547  f1ocnv2d  6053  supisoti  6987  caucvgsrlemoffres  7762  prodge0  8770  un0addcl  9168  un0mulcl  9169  peano2uz2  9319  elfz2nn0  10068  fzind2  10195  expaddzap  10520  expmulzap  10522  cau3lem  11078  climuni  11256  climrecvg1n  11311  fisumcom2  11401  fprodcom2fi  11589  dvdsval2  11752  algcvga  12005  lcmgcdlem  12031  divgcdcoprmex  12056  prmpwdvds  12307  isgrpinv  12756  epttop  12884  cncnp  13024  cnconst  13028  bl2in  13197  metcnpi  13309  metcnpi2  13310  metcnpi3  13311