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  2571  moi2  2907  preq12bg  3753  ordsuc  4540  f1ocnv2d  6042  supisoti  6975  caucvgsrlemoffres  7741  prodge0  8749  un0addcl  9147  un0mulcl  9148  peano2uz2  9298  elfz2nn0  10047  fzind2  10174  expaddzap  10499  expmulzap  10501  cau3lem  11056  climuni  11234  climrecvg1n  11289  fisumcom2  11379  fprodcom2fi  11567  dvdsval2  11730  algcvga  11983  lcmgcdlem  12009  divgcdcoprmex  12034  prmpwdvds  12285  epttop  12730  cncnp  12870  cnconst  12874  bl2in  13043  metcnpi  13155  metcnpi2  13156  metcnpi3  13157