Theorem impr 379

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  reximddv2  2602  moi2  2945  preq12bg  3804  ordsuc  4600  f1ocnv2d  6131  supisoti  7085  caucvgsrlemoffres  7884  prodge0  8898  un0addcl  9299  un0mulcl  9300  peano2uz2  9450  elfz2nn0  10204  fzind2  10332  expaddzap  10692  expmulzap  10694  cau3lem  11296  climuni  11475  climrecvg1n  11530  fisumcom2  11620  fprodcom2fi  11808  dvdsval2  11972  algcvga  12244  lcmgcdlem  12270  divgcdcoprmex  12295  prmpwdvds  12549  isgrpinv  13256  dvdsrcl2  13731  islss4  14014  lspsnel6  14040  epttop  14410  cncnp  14550  cnconst  14554  bl2in  14723  metcnpi  14835  metcnpi2  14836  metcnpi3  14837  perfect  15321  lgsquad2  15408