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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  reximddv2  2655  moi2  3007  preq12bg  3898  ordsuc  4710  f1ocnv2d  6294  f1o3d  6298  suppssrst  6501  suppssrgst  6502  supisoti  7350  caucvgsrlemoffres  8167  prodge0  9186  un0addcl  9600  un0mulcl  9601  peano2uz2  9757  elfz2nn0  10529  fzind2  10668  expaddzap  11033  expmulzap  11035  swrdswrd  11491  cau3lem  11895  climuni  12075  climrecvg1n  12130  fisumcom2  12221  fprodcom2fi  12409  dvdsval2  12573  algcvga  12845  lcmgcdlem  12871  divgcdcoprmex  12896  prmpwdvds  13154  isgrpinv  13908  gsumvalfi  14201  dvdsrcl2  14455  islss4  14768  ellspsn6  14794  epttop  15240  cncnp  15380  cnconst  15384  bl2in  15553  metcnpi  15665  metcnpi2  15666  metcnpi3  15667  perfect  16220  bposlem1  16230  lgsquad2  16321  egrsubgr  16623  clwwlkccat  16761