Theorem impr 371

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  reximddv2  2466  moi2  2774  preq12bg  3567  ordsuc  4308  f1ocnv2d  5729  supisoti  6472  caucvgsrlemoffres  7027  prodge0  7988  un0addcl  8377  un0mulcl  8378  peano2uz2  8524  elfz2nn0  9194  fzind2  9314  expaddzap  9606  expmulzap  9608  cau3lem  10127  climuni  10259  climrecvg1n  10312  dvdsval2  10332  ialgcvga  10566  lcmgcdlem  10592  divgcdcoprmex  10617