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  4712  f1ocnv2d  6297  f1o3d  6301  suppssrst  6505  suppssrgst  6506  supisoti  7357  caucvgsrlemoffres  8174  prodge0  9193  un0addcl  9608  un0mulcl  9609  peano2uz2  9765  elfz2nn0  10537  fzind2  10676  expaddzap  11042  expmulzap  11044  swrdswrd  11500  cau3lem  11904  fiidxsupcl  12019  climuni  12085  climrecvg1n  12140  fisumcom2  12231  fprodcom2fi  12419  dvdsval2  12583  algcvga  12855  lcmgcdlem  12881  divgcdcoprmex  12906  prmpwdvds  13164  isgrpinv  13919  gsumvalfi  14243  dvdsrcl2  14516  islss4  14829  ellspsn6  14855  gsumbagdiagfi  15181  psrass1filem  15182  epttop  15328  cncnp  15468  cnconst  15472  bl2in  15641  metcnpi  15753  metcnpi2  15754  metcnpi3  15755  perfect  16313  bposlem1  16323  lgsquad2  16419  egrsubgr  16721  clwwlkccat  16859