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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reximddv2  2655  moi2  3007  preq12bg  3898  ordsuc  4710  f1ocnv2d  6294  f1o3d  6298  suppssrst  6501  suppssrgst  6502  supisoti  7350  caucvgsrlemoffres  8167  prodge0  9185  un0addcl  9598  un0mulcl  9599  peano2uz2  9755  elfz2nn0  10521  fzind2  10660  expaddzap  11022  expmulzap  11024  swrdswrd  11479  cau3lem  11882  climuni  12061  climrecvg1n  12116  fisumcom2  12207  fprodcom2fi  12395  dvdsval2  12559  algcvga  12831  lcmgcdlem  12857  divgcdcoprmex  12882  prmpwdvds  13136  isgrpinv  13861  gsumvalfi  14154  dvdsrcl2  14408  islss4  14721  ellspsn6  14747  epttop  15193  cncnp  15333  cnconst  15337  bl2in  15506  metcnpi  15618  metcnpi2  15619  metcnpi3  15620  perfect  16121  lgsquad2  16214  egrsubgr  16516  clwwlkccat  16654