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  2615  moi2  2964  preq12bg  3830  ordsuc  4632  f1ocnv2d  6180  supisoti  7145  caucvgsrlemoffres  7955  prodge0  8969  un0addcl  9370  un0mulcl  9371  peano2uz2  9522  elfz2nn0  10276  fzind2  10412  expaddzap  10772  expmulzap  10774  swrdswrd  11203  cau3lem  11591  climuni  11770  climrecvg1n  11825  fisumcom2  11915  fprodcom2fi  12103  dvdsval2  12267  algcvga  12539  lcmgcdlem  12565  divgcdcoprmex  12590  prmpwdvds  12844  isgrpinv  13553  dvdsrcl2  14028  islss4  14311  lspsnel6  14337  epttop  14729  cncnp  14869  cnconst  14873  bl2in  15042  metcnpi  15154  metcnpi2  15155  metcnpi3  15156  perfect  15640  lgsquad2  15727