Theorem impr 372

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 254	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  reximddv2  2479  moi2  2799  preq12bg  3625  ordsuc  4394  f1ocnv2d  5864  supisoti  6761  caucvgsrlemoffres  7408  prodge0  8378  un0addcl  8769  un0mulcl  8770  peano2uz2  8916  elfz2nn0  9589  fzind2  9713  expaddzap  10062  expmulzap  10064  cau3lem  10610  climuni  10744  climrecvg1n  10800  fisumcom2  10895  dvdsval2  11140  algcvga  11374  lcmgcdlem  11400  divgcdcoprmex  11425  epttop  11853