Theorem imp31 256

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp3.1	|- ( ph -> ( ps -> ( ch -> th ) ) )

Assertion

Ref	Expression
imp31	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	imp 124	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
3	2	imp 124	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

This theorem is referenced by:  imp41  353  imp5d  359  impl  380  anassrs  400  an31s  570  con4biddc  858  3imp  1195  3expa  1205  bilukdc  1407  reusv3  4492  dfimafn  5606  funimass4  5608  funimass3  5675  isopolem  5866  smores2  6349  tfrlem9  6374  nnmordi  6571  mulcanpig  7397  elnnz  9330  nzadd  9372  irradd  9714  irrmul  9715  uzsubsubfz  10116  fzo1fzo0n0  10253  elfzonelfzo  10300  infpnlem1  12500  tgcl  14243