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  2637  moi2  2987  preq12bg  3856  ordsuc  4661  f1ocnv2d  6227  supisoti  7209  caucvgsrlemoffres  8020  prodge0  9034  un0addcl  9435  un0mulcl  9436  peano2uz2  9587  elfz2nn0  10347  fzind2  10486  expaddzap  10846  expmulzap  10848  swrdswrd  11287  cau3lem  11676  climuni  11855  climrecvg1n  11910  fisumcom2  12001  fprodcom2fi  12189  dvdsval2  12353  algcvga  12625  lcmgcdlem  12651  divgcdcoprmex  12676  prmpwdvds  12930  isgrpinv  13639  dvdsrcl2  14116  islss4  14399  lspsnel6  14425  epttop  14817  cncnp  14957  cnconst  14961  bl2in  15130  metcnpi  15242  metcnpi2  15243  metcnpi3  15244  perfect  15728  lgsquad2  15815  egrsubgr  16117  clwwlkccat  16255  gfsumval  16701