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  2655  moi2  3007  preq12bg  3896  ordsuc  4708  f1ocnv2d  6288  f1o3d  6292  suppssrst  6495  suppssrgst  6496  supisoti  7344  caucvgsrlemoffres  8161  prodge0  9178  un0addcl  9579  un0mulcl  9580  peano2uz2  9736  elfz2nn0  10502  fzind2  10641  expaddzap  11003  expmulzap  11005  swrdswrd  11460  cau3lem  11863  climuni  12042  climrecvg1n  12097  fisumcom2  12188  fprodcom2fi  12376  dvdsval2  12540  algcvga  12812  lcmgcdlem  12838  divgcdcoprmex  12863  prmpwdvds  13117  isgrpinv  13842  gsumvalfi  14135  dvdsrcl2  14389  islss4  14702  ellspsn6  14728  epttop  15174  cncnp  15314  cnconst  15318  bl2in  15487  metcnpi  15599  metcnpi2  15600  metcnpi3  15601  perfect  16098  lgsquad2  16185  egrsubgr  16487  clwwlkccat  16625