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  2636  moi2  2986  preq12bg  3857  ordsuc  4663  f1ocnv2d  6232  supisoti  7214  caucvgsrlemoffres  8025  prodge0  9039  un0addcl  9440  un0mulcl  9441  peano2uz2  9592  elfz2nn0  10352  fzind2  10491  expaddzap  10851  expmulzap  10853  swrdswrd  11295  cau3lem  11697  climuni  11876  climrecvg1n  11931  fisumcom2  12022  fprodcom2fi  12210  dvdsval2  12374  algcvga  12646  lcmgcdlem  12672  divgcdcoprmex  12697  prmpwdvds  12951  isgrpinv  13660  dvdsrcl2  14137  islss4  14420  lspsnel6  14446  epttop  14843  cncnp  14983  cnconst  14987  bl2in  15156  metcnpi  15268  metcnpi2  15269  metcnpi3  15270  perfect  15754  lgsquad2  15841  egrsubgr  16143  clwwlkccat  16281  gfsumval  16748