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  2647  moi2  2997  preq12bg  3876  ordsuc  4684  f1ocnv2d  6258  suppssrst  6460  suppssrgst  6461  supisoti  7300  caucvgsrlemoffres  8111  prodge0  9124  un0addcl  9525  un0mulcl  9526  peano2uz2  9681  elfz2nn0  10442  fzind2  10581  expaddzap  10941  expmulzap  10943  swrdswrd  11390  cau3lem  11792  climuni  11971  climrecvg1n  12026  fisumcom2  12117  fprodcom2fi  12305  dvdsval2  12469  algcvga  12741  lcmgcdlem  12767  divgcdcoprmex  12792  prmpwdvds  13046  isgrpinv  13756  dvdsrcl2  14233  islss4  14517  lspsnel6  14543  epttop  14942  cncnp  15082  cnconst  15086  bl2in  15255  metcnpi  15367  metcnpi2  15368  metcnpi3  15369  perfect  15856  lgsquad2  15943  egrsubgr  16245  clwwlkccat  16383  gfsumval  16848