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  2599  moi2  2941  preq12bg  3799  ordsuc  4595  f1ocnv2d  6122  supisoti  7069  caucvgsrlemoffres  7860  prodge0  8873  un0addcl  9273  un0mulcl  9274  peano2uz2  9424  elfz2nn0  10178  fzind2  10306  expaddzap  10654  expmulzap  10656  cau3lem  11258  climuni  11436  climrecvg1n  11491  fisumcom2  11581  fprodcom2fi  11769  dvdsval2  11933  algcvga  12189  lcmgcdlem  12215  divgcdcoprmex  12240  prmpwdvds  12493  isgrpinv  13126  dvdsrcl2  13595  islss4  13878  lspsnel6  13904  epttop  14258  cncnp  14398  cnconst  14402  bl2in  14571  metcnpi  14683  metcnpi2  14684  metcnpi3  14685