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  859  3imp  1196  3expa  1206  bilukdc  1416  reusv3  4508  dfimafn  5629  funimass4  5631  funimass3  5698  isopolem  5893  smores2  6382  tfrlem9  6407  nnmordi  6604  mulcanpig  7450  elnnz  9384  nzadd  9427  irradd  9769  irrmul  9770  uzsubsubfz  10171  fzo1fzo0n0  10309  elincfzoext  10324  elfzonelfzo  10361  swrdwrdsymbg  11120  infpnlem1  12715  tgcl  14569