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  2638  moi2  2988  preq12bg  3861  ordsuc  4667  f1ocnv2d  6237  suppssrst  6439  suppssrgst  6440  supisoti  7252  caucvgsrlemoffres  8063  prodge0  9076  un0addcl  9477  un0mulcl  9478  peano2uz2  9631  elfz2nn0  10392  fzind2  10531  expaddzap  10891  expmulzap  10893  swrdswrd  11335  cau3lem  11737  climuni  11916  climrecvg1n  11971  fisumcom2  12062  fprodcom2fi  12250  dvdsval2  12414  algcvga  12686  lcmgcdlem  12712  divgcdcoprmex  12737  prmpwdvds  12991  isgrpinv  13700  dvdsrcl2  14177  islss4  14461  lspsnel6  14487  epttop  14884  cncnp  15024  cnconst  15028  bl2in  15197  metcnpi  15309  metcnpi2  15310  metcnpi3  15311  perfect  15798  lgsquad2  15885  egrsubgr  16187  clwwlkccat  16325  gfsumval  16792