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  2599  moi2  2942  preq12bg  3800  ordsuc  4596  f1ocnv2d  6124  supisoti  7071  caucvgsrlemoffres  7862  prodge0  8875  un0addcl  9276  un0mulcl  9277  peano2uz2  9427  elfz2nn0  10181  fzind2  10309  expaddzap  10657  expmulzap  10659  cau3lem  11261  climuni  11439  climrecvg1n  11494  fisumcom2  11584  fprodcom2fi  11772  dvdsval2  11936  algcvga  12192  lcmgcdlem  12218  divgcdcoprmex  12243  prmpwdvds  12496  isgrpinv  13129  dvdsrcl2  13598  islss4  13881  lspsnel6  13907  epttop  14269  cncnp  14409  cnconst  14413  bl2in  14582  metcnpi  14694  metcnpi2  14695  metcnpi3  14696  lgsquad2  15240